let L be complete LATTICE; :: thesis: ( L is completely-distributive iff for J being non empty set
for K being V8() 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 V8() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup = Inf ) :: thesis: ( ( for J being non empty set
for K being V8() 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 V8() 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 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:
A2: Inf = Sup by A1;
A3: dom K = J by PARTFUN1:def 2;
A4: doms () = (product (doms F)) --> J by Th45;
A6: doms F = K by Th45;
rng () is_<=_than Sup
proof
reconsider J9 = product (doms ()) as non empty set ;
let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in rng () or a <= Sup )
reconsider K9 = J9 --> (product (doms F)) as ManySortedSet of J9 ;
reconsider G = Frege () as DoubleIndexedSet of K9,L ;
assume a in rng () ; :: thesis:
then consider g being Element of J9 such that
A8: a = Inf by WAYBEL_5:14;
reconsider g9 = g as Function ;
deffunc H1( 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) \ H1(j) <> {}
defpred S1[ object , object ] means \$2 in (K . \$1) \ H1(\$1);
assume A10: for j being Element of J holds (K . j) \ H1(j) <> {} ; :: thesis: contradiction
A11: now :: thesis: for j being object st j in J holds
ex k being object st S1[j,k]
let j be object ; :: thesis: ( j in J implies ex k being object st S1[j,k] )
assume j in J ; :: thesis: ex k being object st S1[j,k]
then reconsider i = j as Element of J ;
set k = the Element of (K . i) \ H1(j);
(K . i) \ H1(i) <> {} by A10;
then the Element of (K . i) \ H1(j) in (K . i) \ H1(i) ;
hence ex k being object st S1[j,k] ; :: thesis: verum
end;
consider h being Function such that
A12: ( dom h = J & ( for j being object st j in J holds
S1[j,h . j] ) ) from
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) \ H1(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 ;
g9 . h in (doms ()) . h by ;
then reconsider j = g9 . h as Element of J by A4;
( h . (g9 . h) in H1(j) & h . j in (K . j) \ H1(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) \ H1(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 H1(j) by ;
then consider f being Element of product (doms F) such that
A17: u = f . (g9 . f) and
A18: g9 . f = j ;
A: ( G . g = () .. g9 & () . 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 ;
j in (dom F) /\ (dom f) by ;
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 () = product (doms F) by PARTFUN1:def 2;
consider gg1 being Function such that
BB: ( g = gg1 & dom gg1 = dom (doms ()) & ( for y being object st y in dom (doms ()) holds
gg1 . y in (doms ()) . y ) ) by CARD_3:def 5;
f in dom () by A27;
then f in dom (doms ()) by FUNCT_6:def 2;
then f in (dom ()) /\ (dom g9) by ;
then f in dom (() .. g9) by PRALG_1:def 19;
then (G . g) . f = (F .. f) . j by ;
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 ; :: 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 ;
then a <= inf (rng (F . j)) by ;
then A20: a <= Inf by YELLOW_2:def 6;
Inf in rng () by WAYBEL_5:14;
then Inf <= sup (rng ()) by YELLOW_2:22;
then a <= sup (rng ()) by ;
hence a <= Sup by YELLOW_2:def 5; :: thesis: verum
end;
then sup (rng ()) <= Sup by YELLOW_0:32;
then A21: Sup <= Sup by YELLOW_2:def 5;
Sup <= Inf by Th47;
hence Sup = Inf by ; :: thesis: verum
end;
assume A22: for J being non empty set
for K being V8() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup = Inf ; :: thesis:
thus L is complete ; :: according to WAYBEL_5:def 3 :: thesis: for b1 being set
for b2 being set
for b3 being ManySortedFunction of b2,b1 --> the carrier of L holds //\ ((\// (b3,L)),L) = \\/ ((/\\ ((Frege b3),L)),L)

let J be non empty set ; :: thesis: for b1 being set
for b2 being ManySortedFunction of b1,J --> the carrier of L holds //\ ((\// (b2,L)),L) = \\/ ((/\\ ((Frege b2),L)),L)

let K be V8() ManySortedSet of J; :: thesis: for b1 being ManySortedFunction of K,J --> the carrier of L holds //\ ((\// (b1,L)),L) = \\/ ((/\\ ((Frege b1),L)),L)
let F be DoubleIndexedSet of K,L; :: thesis: //\ ((\// (F,L)),L) = \\/ ((/\\ ((),L)),L)
A23: dom K = J by PARTFUN1:def 2;
A24: doms () = (product (doms F)) --> J by Th45;
A25: dom F = J by PARTFUN1:def 2;
A26: doms F = K by Th45;
A27: dom () = product (doms F) by PARTFUN1:def 2;
rng () is_>=_than Inf
proof
reconsider J9 = product (doms ()) as non empty set ;
let a be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not a in rng () or Inf <= a )
reconsider K9 = J9 --> (product (doms F)) as ManySortedSet of J9 ;
reconsider G = Frege () as DoubleIndexedSet of K9,L ;
assume a in rng () ; :: thesis:
then consider g being Element of J9 such that
A28: a = Sup by WAYBEL_5:14;
reconsider g9 = g as Function ;
deffunc H1( 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) \ H1(j) <> {}
defpred S1[ object , object ] means \$2 in (K . \$1) \ H1(\$1);
assume A30: for j being Element of J holds (K . j) \ H1(j) <> {} ; :: thesis: contradiction
A31: now :: thesis: for j being object st j in J holds
ex k being object st S1[j,k]
let j be object ; :: thesis: ( j in J implies ex k being object st S1[j,k] )
assume j in J ; :: thesis: ex k being object st S1[j,k]
then reconsider i = j as Element of J ;
set k = the Element of (K . i) \ H1(j);
(K . i) \ H1(i) <> {} by A30;
then the Element of (K . i) \ H1(j) in (K . i) \ H1(i) ;
hence ex k being object st S1[j,k] ; :: thesis: verum
end;
consider h being Function such that
A32: ( dom h = J & ( for j being object st j in J holds
S1[j,h . j] ) ) from
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) \ H1(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 ;
g9 . h in (doms ()) . h by ;
then reconsider j = g9 . h as Element of J by A24;
( h . (g9 . h) in H1(j) & h . j in (K . j) \ H1(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) \ H1(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 H1(j) by ;
then consider f being Element of product (doms F) such that
A37: u = f . (g9 . f) and
A38: g9 . f = j ;
a37: ( G . g = () .. g9 & () . 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 ;
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 ()) & ( for y being object st y in dom (doms ()) holds
gg1 . y in (doms ()) . y ) ) by CARD_3:def 5;
f in dom () by A27;
then f in dom g9 by ;
then f in (dom ()) /\ (dom g9) by ;
then a38: f in dom (() .. g9) by PRALG_1:def 19;
(G . g) . f = (() . f) . (g9 . f) by ;
then A39: (G . g) . f = z by ;
( dom (G . g) = K9 . g & K9 . g = product (doms F) ) by FUNCT_2:def 1;
hence z in rng (G . g) by ; :: 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 ;
then a >= sup (rng (F . j)) by ;
then A40: a >= Sup by YELLOW_2:def 5;
Sup in rng () by WAYBEL_5:14;
then Sup >= inf (rng ()) by YELLOW_2:22;
then a >= inf (rng ()) by ;
hence Inf <= a by YELLOW_2:def 6; :: thesis: verum
end;
then inf (rng ()) >= Inf by YELLOW_0:33;
then A41: Inf >= Inf by YELLOW_2:def 6;
( Inf >= Sup & Sup = Inf ) by ;
hence //\ ((\// (F,L)),L) = \\/ ((/\\ ((),L)),L) by ; :: thesis: verum