let L be complete LATTICE; :: thesis: for J being non empty set

for K being V8() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Sup <= Inf

let J be non empty set ; :: thesis: for K being V8() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Sup <= Inf

let K be V8() ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,L holds Sup <= Inf

let F be DoubleIndexedSet of K,L; :: thesis: Sup <= Inf

Inf is_>=_than rng (Infs )

hence Sup <= Inf by YELLOW_2:def 5; :: thesis: verum

for K being V8() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Sup <= Inf

let J be non empty set ; :: thesis: for K being V8() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Sup <= Inf

let K be V8() ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,L holds Sup <= Inf

let F be DoubleIndexedSet of K,L; :: thesis: Sup <= Inf

Inf is_>=_than rng (Infs )

proof

then
sup (rng (Infs )) <= Inf
by YELLOW_0:32;
let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in rng (Infs ) or x <= Inf )

assume x in rng (Infs ) ; :: thesis: x <= Inf

then consider a being Element of J such that

A1: x = Inf by WAYBEL_5:14;

A2: x = inf (rng (F . a)) by A1, YELLOW_2:def 6;

x is_<=_than rng (Sups )

hence x <= Inf by YELLOW_2:def 6; :: thesis: verum

end;assume x in rng (Infs ) ; :: thesis: x <= Inf

then consider a being Element of J such that

A1: x = Inf by WAYBEL_5:14;

A2: x = inf (rng (F . a)) by A1, YELLOW_2:def 6;

x is_<=_than rng (Sups )

proof

then
x <= inf (rng (Sups ))
by YELLOW_0:33;
reconsider J9 = product (doms F) as non empty set ;

let y be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not y in rng (Sups ) or x <= y )

reconsider K9 = J9 --> J as ManySortedSet of J9 ;

reconsider G = Frege F as DoubleIndexedSet of K9,L ;

assume y in rng (Sups ) ; :: thesis: x <= y

then consider f being Element of J9 such that

A3: y = Sup by WAYBEL_5:14;

reconsider f = f as Element of product (doms F) ;

A4: ( dom F = J & dom (Frege F) = product (doms F) ) by PARTFUN1:def 2;

then f . a in dom (F . a) by WAYBEL_5:9;

then reconsider j = f . a as Element of K . a ;

A5: (F . a) . j in rng ((Frege F) . f) by A4, WAYBEL_5:9;

j in dom (F . a) by A4, WAYBEL_5:9;

then (F . a) . j in rng (F . a) by FUNCT_1:def 3;

then A6: x <= (F . a) . j by A2, YELLOW_2:22;

y = sup (rng ((Frege F) . f)) by A3, YELLOW_2:def 5;

then (F . a) . j <= y by A5, YELLOW_2:22;

hence x <= y by A6, ORDERS_2:3; :: thesis: verum

end;let y be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not y in rng (Sups ) or x <= y )

reconsider K9 = J9 --> J as ManySortedSet of J9 ;

reconsider G = Frege F as DoubleIndexedSet of K9,L ;

assume y in rng (Sups ) ; :: thesis: x <= y

then consider f being Element of J9 such that

A3: y = Sup by WAYBEL_5:14;

reconsider f = f as Element of product (doms F) ;

A4: ( dom F = J & dom (Frege F) = product (doms F) ) by PARTFUN1:def 2;

then f . a in dom (F . a) by WAYBEL_5:9;

then reconsider j = f . a as Element of K . a ;

A5: (F . a) . j in rng ((Frege F) . f) by A4, WAYBEL_5:9;

j in dom (F . a) by A4, WAYBEL_5:9;

then (F . a) . j in rng (F . a) by FUNCT_1:def 3;

then A6: x <= (F . a) . j by A2, YELLOW_2:22;

y = sup (rng ((Frege F) . f)) by A3, YELLOW_2:def 5;

then (F . a) . j <= y by A5, YELLOW_2:22;

hence x <= y by A6, ORDERS_2:3; :: thesis: verum

hence x <= Inf by YELLOW_2:def 6; :: thesis: verum

hence Sup <= Inf by YELLOW_2:def 5; :: thesis: verum