let L be complete LATTICE; :: thesis: ( L is completely-distributive iff for J being non empty set
for K being V5() ManySortedSet of
for F being DoubleIndexedSet of K,L holds Sup = Inf )
thus ( L is completely-distributive implies for J being non empty set
for K being V5() ManySortedSet of
for F being DoubleIndexedSet of K,L holds Sup = Inf ) :: thesis: ( ( for J being non empty set
for K being V5() ManySortedSet of
for F being DoubleIndexedSet of K,L holds Sup = Inf ) implies L is completely-distributive )

proof

assume that
L is complete and
A1: for J being non empty set
for K being V5() ManySortedSet of
for F being DoubleIndexedSet of K,L holds Inf = Sup ; :: according to WAYBEL_5:def 3 :: thesis: for J being non empty set
for K being V5() ManySortedSet of
for F being DoubleIndexedSet of K,L holds Sup = Inf
let J be non empty set ; :: thesis: for K being V5() ManySortedSet of
for F being DoubleIndexedSet of K,L holds Sup = Inf
let K be V5() ManySortedSet of ; :: thesis: for F being DoubleIndexedSet of K,L holds Sup = Inf
let F be DoubleIndexedSet of K,L; :: thesis: Sup = Inf
A2: Sup <= Inf by Th47;
A3: Inf = Sup by A1;
A4: ( dom (Frege F) = product (doms F) & doms F = K & dom K = J & doms (Frege F) = (product (doms F)) --> J & dom F = J & dom (Frege (Frege F)) = product (doms (Frege F)) ) by Th45, PARTFUN1:def 4;
rng (Infs ) is_<=_than Sup

proof

let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in rng (Infs ) or a <= Sup )
assume A5: a in rng (Infs ) ; :: thesis: a <= Sup
reconsider J' = product (doms (Frege F)) as non empty set ;
reconsider K' = J' --> (product (doms F)) as ManySortedSet of ;
reconsider G = Frege (Frege F) as DoubleIndexedSet of K',L ;
consider g being Element of J' such that
A6: a = Inf by A5, WAYBEL_5:14;
reconsider g' = g as Function ;
deffunc H₁( set ) -> set = { (f . (g' . f)) where f is Element of product (doms F) : g' . f = $1 } ;
A7: ( (J' --> J) . g = J & dom ((product (doms F)) --> J) = product (doms F) ) by FUNCOP_1:13, FUNCOP_1:19;

now

assume A8: for j being Element of J holds (K . j) \ H₁(j) <> {} ; :: thesis: contradiction
defpred S₁[ set , set ] means $2 in (K . $1) \ H₁($1);

A9: now

let j be set ; :: thesis: ( j in J implies ex k being set st S₁[j,k] )
assume j in J ; :: thesis: ex k being set st S₁[j,k]
then reconsider i = j as Element of J ;
consider k being Element of (K . i) \ H₁(j);
(K . i) \ H₁(i) <> {} by A8;
then k in (K . i) \ H₁(i) ;
hence ex k being set st S₁[j,k] ; :: thesis: verum

end;

consider h being Function such that
A10: ( dom h = J & ( for j being set st j in J holds
S₁[j,h . j] ) ) from CLASSES1:sch 1(A9);

now

let j be set ; :: thesis: ( j in J implies h . j in (doms F) . j )
assume j in J ; :: thesis: h . j in (doms F) . j
then h . j in (K . j) \ H₁(j) by A10;
hence h . j in (doms F) . j by A4; :: thesis: verum

end;

then reconsider h = h as Element of product (doms F) by A4, A10, CARD_3:18;
g' . h in (doms (Frege F)) . h by A4, A7, CARD_3:18;
then reconsider j = g' . h as Element of J by A4, FUNCOP_1:13;
( h . (g' . h) in H₁(j) & h . j in (K . j) \ H₁(j) ) by A10;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum

end;

then consider j being Element of J such that
A11: (K . j) \ H₁(j) = {} ;
A12: ( ex_inf_of rng (G . g),L & ex_inf_of rng (F . j),L ) by YELLOW_0:17;
rng (F . j) c= rng (G . g)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (F . j) or z in rng (G . g) )
assume z in rng (F . j) ; :: thesis: z in rng (G . g)
then consider u being set such that
A13: ( u in dom (F . j) & z = (F . j) . u ) by FUNCT_1:def 5;
reconsider u = u as Element of K . j by A13;
u in H₁(j) by A11, XBOOLE_0:def 5;
then consider f being Element of product (doms F) such that
A14: ( u = f . (g' . f) & g' . f = j ) ;
A15: ( dom (G . g) = K' . g & K' . g = product (doms F) ) by FUNCOP_1:13, FUNCT_2:def 1;
( G . g = (Frege F) .. g' & (Frege F) . f = F .. f ) by PRALG_2:def 8;
then (G . g) . f = (F .. f) . j by A4, A14, PRALG_1:def 17;
then (G . g) . f = z by A4, A13, A14, PRALG_1:def 17;
hence z in rng (G . g) by A15, FUNCT_1:def 5; :: thesis: verum

end;

then inf (rng (G . g)) <= inf (rng (F . j)) by A12, YELLOW_0:35;
then ( a <= inf (rng (F . j)) & Inf in rng (Infs ) ) by A6, WAYBEL_5:14, YELLOW_2:def 6;
then ( a <= Inf & Inf <= sup (rng (Infs )) ) by YELLOW_2:24, YELLOW_2:def 6;
then a <= sup (rng (Infs )) by ORDERS_2:26;
hence a <= Sup by YELLOW_2:def 5; :: thesis: verum

end;

then sup (rng (Infs )) <= Sup by YELLOW_0:32;
then Sup <= Sup by YELLOW_2:def 5;
hence Sup = Inf by A2, A3, ORDERS_2:25; :: thesis: verum

end;

assume A16: for J being non empty set
for K being V5() ManySortedSet of
for F being DoubleIndexedSet of K,L holds Sup = Inf ; :: thesis: L is completely-distributive
thus L is complete ; :: according to WAYBEL_5:def 3 :: thesis: for b₁ being set
for b₂ being set
for b₃ being ManySortedFunction of b₂,b₁ --> the carrier of L holds //\ (\// b₃,L),L = \\/ (/\\ (Frege b₃),L),L
let J be non empty set ; :: thesis: for b₁ being set
for b₂ being ManySortedFunction of b₁,J --> the carrier of L holds //\ (\// b₂,L),L = \\/ (/\\ (Frege b₂),L),L
let K be V5() ManySortedSet of ; :: thesis: for b₁ being ManySortedFunction of K,J --> the carrier of L holds //\ (\// b₁,L),L = \\/ (/\\ (Frege b₁),L),L
let F be DoubleIndexedSet of K,L; :: thesis: //\ (\// F,L),L = \\/ (/\\ (Frege F),L),L
A17: Inf >= Sup by WAYBEL_5:16;
A18: Sup = Inf by A16;
A19: ( dom (Frege F) = product (doms F) & doms F = K & dom K = J & doms (Frege F) = (product (doms F)) --> J & dom F = J & dom (Frege (Frege F)) = product (doms (Frege F)) ) by Th45, PARTFUN1:def 4;
rng (Sups ) is_>=_than Inf

proof

let a be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not a in rng (Sups ) or Inf <= a )
assume A20: a in rng (Sups ) ; :: thesis: Inf <= a
reconsider J' = product (doms (Frege F)) as non empty set ;
reconsider K' = J' --> (product (doms F)) as ManySortedSet of ;
reconsider G = Frege (Frege F) as DoubleIndexedSet of K',L ;
consider g being Element of J' such that
A21: a = Sup by A20, WAYBEL_5:14;
reconsider g' = g as Function ;
deffunc H₁( set ) -> set = { (f . (g' . f)) where f is Element of product (doms F) : g' . f = $1 } ;
A22: ( (J' --> J) . g = J & dom ((product (doms F)) --> J) = product (doms F) ) by FUNCOP_1:13, FUNCOP_1:19;

now

assume A23: for j being Element of J holds (K . j) \ H₁(j) <> {} ; :: thesis: contradiction
defpred S₁[ set , set ] means $2 in (K . $1) \ H₁($1);

A24: now

let j be set ; :: thesis: ( j in J implies ex k being set st S₁[j,k] )
assume j in J ; :: thesis: ex k being set st S₁[j,k]
then reconsider i = j as Element of J ;
consider k being Element of (K . i) \ H₁(j);
(K . i) \ H₁(i) <> {} by A23;
then k in (K . i) \ H₁(i) ;
hence ex k being set st S₁[j,k] ; :: thesis: verum

end;

consider h being Function such that
A25: ( dom h = J & ( for j being set st j in J holds
S₁[j,h . j] ) ) from CLASSES1:sch 1(A24);

now

let j be set ; :: thesis: ( j in J implies h . j in (doms F) . j )
assume j in J ; :: thesis: h . j in (doms F) . j
then h . j in (K . j) \ H₁(j) by A25;
hence h . j in (doms F) . j by A19; :: thesis: verum

end;

then reconsider h = h as Element of product (doms F) by A19, A25, CARD_3:18;
g' . h in (doms (Frege F)) . h by A19, A22, CARD_3:18;
then reconsider j = g' . h as Element of J by A19, FUNCOP_1:13;
( h . (g' . h) in H₁(j) & h . j in (K . j) \ H₁(j) ) by A25;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum

end;

then consider j being Element of J such that
A26: (K . j) \ H₁(j) = {} ;
A27: ( ex_sup_of rng (G . g),L & ex_sup_of rng (F . j),L ) by YELLOW_0:17;
rng (F . j) c= rng (G . g)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (F . j) or z in rng (G . g) )
assume z in rng (F . j) ; :: thesis: z in rng (G . g)
then consider u being set such that
A28: ( u in dom (F . j) & z = (F . j) . u ) by FUNCT_1:def 5;
reconsider u = u as Element of K . j by A28;
u in H₁(j) by A26, XBOOLE_0:def 5;
then consider f being Element of product (doms F) such that
A29: ( u = f . (g' . f) & g' . f = j ) ;
A30: ( dom (G . g) = K' . g & K' . g = product (doms F) ) by FUNCOP_1:13, FUNCT_2:def 1;
( G . g = (Frege F) .. g' & (Frege F) . f = F .. f ) by PRALG_2:def 8;
then (G . g) . f = (F .. f) . j by A19, A29, PRALG_1:def 17;
then (G . g) . f = z by A19, A28, A29, PRALG_1:def 17;
hence z in rng (G . g) by A30, FUNCT_1:def 5; :: thesis: verum

end;

then sup (rng (G . g)) >= sup (rng (F . j)) by A27, YELLOW_0:34;
then ( a >= sup (rng (F . j)) & Sup in rng (Sups ) ) by A21, WAYBEL_5:14, YELLOW_2:def 5;
then ( a >= Sup & Sup >= inf (rng (Sups )) ) by YELLOW_2:24, YELLOW_2:def 5;
then a >= inf (rng (Sups )) by ORDERS_2:26;
hence Inf <= a by YELLOW_2:def 6; :: thesis: verum

end;

then inf (rng (Sups )) >= Inf by YELLOW_0:33;
then Inf >= Inf by YELLOW_2:def 6;
hence //\ (\// F,L),L = \\/ (/\\ (Frege F),L),L by A17, A18, ORDERS_2:25; :: thesis: verum