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: Inf = Sup by A1;
A3: dom K = J by PARTFUN1:def 4;
A4: doms (Frege F) = (product (doms F)) --> J by Th45;
A5: dom F = J by PARTFUN1:def 4;
A6: doms F = K by Th45;
A7: dom (Frege F) = product (doms F) by PARTFUN1:def 4;
rng (Infs ) is_<=_than Sup

proof

reconsider J' = product (doms (Frege F)) as non empty set ;
let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in rng (Infs ) or a <= Sup )
reconsider K' = J' --> (product (doms F)) as ManySortedSet of ;
reconsider G = Frege (Frege F) as DoubleIndexedSet of K',L ;
assume a in rng (Infs ) ; :: thesis: a <= Sup
then consider g being Element of J' such that
A8: a = Inf by 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 } ;
A9: dom ((product (doms F)) --> J) = product (doms F) by FUNCOP_1:19;

now

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

A11: 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 A10;
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
A12: ( dom h = J & ( for j being set st j in J holds
S₁[j,h . j] ) ) from CLASSES1:sch 1(A11);

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 A12;
hence h . j in (doms F) . j by A6; :: thesis: verum

end;

then reconsider h = h as Element of product (doms F) by A6, A3, A12, CARD_3:18;
g' . h in (doms (Frege F)) . h by A4, A9, 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 A12;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum

end;

then consider j being Element of J such that
A13: (K . j) \ H₁(j) = {} ;
A14: 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
A15: u in dom (F . j) and
A16: z = (F . j) . u by FUNCT_1:def 5;
reconsider u = u as Element of K . j by A15;
u in H₁(j) by A13, XBOOLE_0:def 5;
then consider f being Element of product (doms F) such that
A17: u = f . (g' . f) and
A18: g' . f = j ;
( G . g = (Frege F) .. g' & (Frege F) . f = F .. f ) by PRALG_2:def 8;
then (G . g) . f = (F .. f) . j by A7, A18, PRALG_1:def 17;
then A19: (G . g) . f = z by A5, A16, A17, A18, PRALG_1:def 17;
( dom (G . g) = K' . g & K' . g = product (doms F) ) by FUNCOP_1:13, FUNCT_2:def 1;
hence z in rng (G . g) by A19, FUNCT_1:def 5; :: thesis: verum

end;

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

end;

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

end;

assume A22: 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
A23: dom K = J by PARTFUN1:def 4;
A24: doms (Frege F) = (product (doms F)) --> J by Th45;
A25: dom F = J by PARTFUN1:def 4;
A26: doms F = K by Th45;
A27: dom (Frege F) = product (doms F) by PARTFUN1:def 4;
rng (Sups ) is_>=_than Inf

proof

reconsider J' = product (doms (Frege F)) as non empty set ;
let a be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not a in rng (Sups ) or Inf <= a )
reconsider K' = J' --> (product (doms F)) as ManySortedSet of ;
reconsider G = Frege (Frege F) as DoubleIndexedSet of K',L ;
assume a in rng (Sups ) ; :: thesis: Inf <= a
then consider g being Element of J' such that
A28: a = Sup by 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 } ;
A29: dom ((product (doms F)) --> J) = product (doms F) by FUNCOP_1:19;

now

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

A31: 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 A30;
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
A32: ( dom h = J & ( for j being set st j in J holds
S₁[j,h . j] ) ) from CLASSES1:sch 1(A31);

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 A32;
hence h . j in (doms F) . j by A26; :: thesis: verum

end;

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

end;

then consider j being Element of J such that
A33: (K . j) \ H₁(j) = {} ;
A34: 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
A35: u in dom (F . j) and
A36: z = (F . j) . u by FUNCT_1:def 5;
reconsider u = u as Element of K . j by A35;
u in H₁(j) by A33, XBOOLE_0:def 5;
then consider f being Element of product (doms F) such that
A37: u = f . (g' . f) and
A38: g' . f = j ;
( G . g = (Frege F) .. g' & (Frege F) . f = F .. f ) by PRALG_2:def 8;
then (G . g) . f = (F .. f) . j by A27, A38, PRALG_1:def 17;
then A39: (G . g) . f = z by A25, A36, A37, A38, PRALG_1:def 17;
( dom (G . g) = K' . g & K' . g = product (doms F) ) by FUNCOP_1:13, FUNCT_2:def 1;
hence z in rng (G . g) by A39, FUNCT_1:def 5; :: thesis: verum

end;

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

end;

then inf (rng (Sups )) >= Inf by YELLOW_0:33;
then A41: Inf >= Inf by YELLOW_2:def 6;
( Inf >= Sup & Sup = Inf ) by A22, WAYBEL_5:16;
hence //\ (\// F,L),L = \\/ (/\\ (Frege F),L),L by A41, ORDERS_2:25; :: thesis: verum