let L be complete LATTICE; :: thesis: ( L is completely-distributive iff for J being non empty set
for K being non-empty ManySortedSet of J
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 non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup = Inf ) :: thesis: ( ( for J being non empty set
for K being non-empty ManySortedSet of J
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 non-empty ManySortedSet of J
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 non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup = Inf
let J be non empty set ; :: thesis: for K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup = Inf
let K be non-empty ManySortedSet of J; :: 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 2;
A4: doms (Frege F) = (product (doms F)) --> J by Th45;
A6: doms F = K by Th45;
rng (Infs ) is_<=_than Sup

proof

reconsider J9 = 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 K9 = J9 --> (product (doms F)) as ManySortedSet of J9 ;
reconsider G = Frege (Frege F) as DoubleIndexedSet of K9,L ;
assume a in rng (Infs ) ; :: thesis: a <= Sup
then consider g being Element of J9 such that
A8: a = Inf by WAYBEL_5:14;
reconsider g9 = g as Function ;
deffunc H₁( object ) -> set = { (f . (g9 . f)) where f is Element of product (doms F) : g9 . f = $1 } ;
A9: dom ((product (doms F)) --> J) = product (doms F) ;

now :: thesis: not for j being Element of J holds (K . j) \ H₁(j) <> {}

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

A11: now :: thesis: for j being object st j in J holds
ex k being object st S₁[j,k]

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

end;

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

now :: thesis: for j being object st j in J holds
h . j in (doms F) . j

let j be object ; :: 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:9;
g9 . h in (doms (Frege F)) . h by A4, A9, CARD_3:9;
then reconsider j = g9 . h as Element of J by A4;
( h . (g9 . 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 object ; :: 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 object such that
A15: u in dom (F . j) and
A16: z = (F . j) . u by FUNCT_1:def 3;
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 . (g9 . f) and
A18: g9 . f = j ;
A: ( G . g = (Frege F) .. g9 & (Frege F) . f = F .. f ) by PRALG_2:def 2;
consider gg being Function such that
BB: ( f = gg & dom gg = dom (doms F) & ( for y being object st y in dom (doms F) holds
gg . y in (doms F) . y ) ) by CARD_3:def 5;
A25: dom F = J by PARTFUN1:def 2;
BC: dom f = dom F by FUNCT_6:def 2, BB;
j in (dom F) /\ (dom f) by A25, BC;
then j in dom (F .. f) by PRALG_1:def 19;
then WW: (F .. f) . j = (F . j) . (f . j) by PRALG_1:def 19;
A27: dom (Frege F) = product (doms F) by PARTFUN1:def 2;
consider gg1 being Function such that
BB: ( g = gg1 & dom gg1 = dom (doms (Frege F)) & ( for y being object st y in dom (doms (Frege F)) holds
gg1 . y in (doms (Frege F)) . y ) ) by CARD_3:def 5;
f in dom (Frege F) by A27;
then f in dom (doms (Frege F)) by FUNCT_6:def 2;
then f in (dom (Frege F)) /\ (dom g9) by A27, BB, XBOOLE_0:def 4;
then f in dom ((Frege F) .. g9) by PRALG_1:def 19;
then (G . g) . f = (F .. f) . j by A18, PRALG_1:def 19, A;
then A19: (G . g) . f = z by A16, A17, A18, WW;
( dom (G . g) = K9 . g & K9 . g = product (doms F) ) by FUNCT_2:def 1;
hence z in rng (G . g) by A19, FUNCT_1:def 3; :: 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:22;
then a <= sup (rng (Infs )) by A20, ORDERS_2:3;
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:2; :: thesis: verum

end;

assume A22: for J being non empty set
for K being non-empty ManySortedSet of J
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 non-empty ManySortedSet of J; :: 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 2;
A24: doms (Frege F) = (product (doms F)) --> J by Th45;
A25: dom F = J by PARTFUN1:def 2;
A26: doms F = K by Th45;
A27: dom (Frege F) = product (doms F) by PARTFUN1:def 2;
rng (Sups ) is_>=_than Inf

proof

reconsider J9 = 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 K9 = J9 --> (product (doms F)) as ManySortedSet of J9 ;
reconsider G = Frege (Frege F) as DoubleIndexedSet of K9,L ;
assume a in rng (Sups ) ; :: thesis: Inf <= a
then consider g being Element of J9 such that
A28: a = Sup by WAYBEL_5:14;
reconsider g9 = g as Function ;
deffunc H₁( object ) -> set = { (f . (g9 . f)) where f is Element of product (doms F) : g9 . f = $1 } ;
A29: dom ((product (doms F)) --> J) = product (doms F) ;

now :: thesis: not for j being Element of J holds (K . j) \ H₁(j) <> {}

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

A31: now :: thesis: for j being object st j in J holds
ex k being object st S₁[j,k]

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

end;

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

now :: thesis: for j being object st j in J holds
h . j in (doms F) . j

let j be object ; :: 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:9;
g9 . h in (doms (Frege F)) . h by A24, A29, CARD_3:9;
then reconsider j = g9 . h as Element of J by A24;
( h . (g9 . 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 object ; :: 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 object such that
A35: u in dom (F . j) and
A36: z = (F . j) . u by FUNCT_1:def 3;
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 . (g9 . f) and
A38: g9 . f = j ;
a37: ( G . g = (Frege F) .. g9 & (Frege F) . f = F .. f ) by PRALG_2:def 2;
consider gg being Function such that
BB: ( f = gg & dom gg = dom (doms F) & ( for y being object st y in dom (doms F) holds
gg . y in (doms F) . y ) ) by CARD_3:def 5;
dom F = dom f by BB, FUNCT_6:def 2;
then j in (dom F) /\ (dom f) by A25;
then Z1: j in dom (F .. f) by PRALG_1:def 19;
consider gg1 being Function such that
BB: ( g = gg1 & dom gg1 = dom (doms (Frege F)) & ( for y being object st y in dom (doms (Frege F)) holds
gg1 . y in (doms (Frege F)) . y ) ) by CARD_3:def 5;
f in dom (Frege F) by A27;
then f in dom g9 by BB, FUNCT_6:def 2;
then f in (dom (Frege F)) /\ (dom g9) by A27, XBOOLE_0:def 4;
then a38: f in dom ((Frege F) .. g9) by PRALG_1:def 19;
(G . g) . f = ((Frege F) . f) . (g9 . f) by a37, a38, PRALG_1:def 19;
then A39: (G . g) . f = z by Z1, A36, a37, A37, A38, PRALG_1:def 19;
( dom (G . g) = K9 . g & K9 . g = product (doms F) ) by FUNCT_2:def 1;
hence z in rng (G . g) by A39, FUNCT_1:def 3; :: 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:22;
then a >= inf (rng (Sups )) by A40, ORDERS_2:3;
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:2; :: thesis: verum