let L be complete continuous LATTICE; :: thesis: ( ( for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) ) ) implies L is completely-distributive )

assume A1: for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) ) ; :: 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 V11() 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)
set l = Inf ;
set X = (waybelow ()) /\ (PRIME (L ~));
A2: (waybelow ()) /\ (PRIME (L ~)) c= waybelow () by XBOOLE_1:17;
reconsider X = (waybelow ()) /\ (PRIME (L ~)) as Subset of L ;
A3: dom F = J by PARTFUN1:def 2;
A4: for x being Element of L st x in X holds
x is co-prime
proof
let x be Element of L; :: thesis: ( x in X implies x is co-prime )
assume x in X ; :: thesis: x is co-prime
then x in PRIME (L ~) by XBOOLE_0:def 4;
then x ~ is prime by Def7;
hence x is co-prime ; :: thesis: verum
end;
A5: inf (rng ()) = Inf by YELLOW_2:def 6;
X is_<=_than Sup
proof
let p be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not p in X or p <= Sup )
defpred S1[ object , object ] means ( \$2 in K . \$1 & [p,((F . \$1) . \$2)] in the InternalRel of L );
assume A6: p in X ; :: thesis:
A7: for j being object st j in J holds
ex k being object st S1[j,k]
proof
let j1 be object ; :: thesis: ( j1 in J implies ex k being object st S1[j1,k] )
assume j1 in J ; :: thesis: ex k being object st S1[j1,k]
then reconsider j = j1 as Element of J ;
set k = the Element of K . j;
dom () = J by ;
then A8: (Sups ) . j in rng () by FUNCT_1:def 3;
A9: ( p << Inf & Sup = sup (rng (F . j)) ) by ;
Sup = () . j by ;
then Inf <= Sup by ;
then consider A being finite Subset of L such that
A10: A c= rng (F . j) and
A11: p <= sup A by ;
( ex_sup_of A,L & ex_sup_of A \/ {((F . j) . the Element of K . j)},L ) by YELLOW_0:17;
then sup A <= sup (A \/ {((F . j) . the Element of K . j)}) by ;
then A12: p <= sup (A \/ {((F . j) . the Element of K . j)}) by ;
p is co-prime by A4, A6;
then consider a being Element of L such that
A13: a in A \/ {((F . j) . the Element of K . j)} and
A14: p <= a by ;
per cases ( a in A or a in {((F . j) . the Element of K . j)} ) by ;
suppose a in A ; :: thesis: ex k being object st S1[j1,k]
then consider k1 being object such that
A15: k1 in dom (F . j) and
A16: a = (F . j) . k1 by ;
reconsider k1 = k1 as Element of K . j by A15;
[p,((F . j) . k1)] in the InternalRel of L by ;
hence ex k being object st S1[j1,k] ; :: thesis: verum
end;
suppose a in {((F . j) . the Element of K . j)} ; :: thesis: ex k being object st S1[j1,k]
then a = (F . j) . the Element of K . j by TARSKI:def 1;
then [p,((F . j) . the Element of K . j)] in the InternalRel of L by ;
hence ex k being object st S1[j1,k] ; :: thesis: verum
end;
end;
end;
consider f1 being Function such that
A17: dom f1 = J and
A18: for j being object st j in J holds
S1[j,f1 . j] from
now :: thesis: for g being object st g in dom (doms F) holds
g in dom f1
let g be object ; :: thesis: ( g in dom (doms F) implies g in dom f1 )
assume g in dom (doms F) ; :: thesis: g in dom f1
then g in dom F by FUNCT_6:def 2;
hence g in dom f1 by A17; :: thesis: verum
end;
then A19: dom (doms F) c= dom f1 ;
for g being object st g in dom f1 holds
g in dom (doms F) by ;
then dom f1 c= dom (doms F) ;
then A20: dom f1 = dom (doms F) by A19;
A21: for b being object st b in dom (doms F) holds
f1 . b in (doms F) . b
proof
let b be object ; :: thesis: ( b in dom (doms F) implies f1 . b in (doms F) . b )
assume A22: b in dom (doms F) ; :: thesis: f1 . b in (doms F) . b
then A23: F . b is Function of (K . b), the carrier of L by ;
(doms F) . b = dom (F . b) by
.= K . b by ;
hence f1 . b in (doms F) . b by A17, A18, A19, A22; :: thesis: verum
end;
then reconsider D = product (doms F) as non empty set by ;
reconsider f = f1 as Element of product (doms F) by ;
A24: f1 in product (doms F) by ;
p is_<=_than rng (() . f)
proof
let b be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not b in rng (() . f) or p <= b )
assume b in rng (() . f) ; :: thesis: p <= b
then consider a being object such that
A25: a in dom (() . f) and
A26: b = (() . f) . a by FUNCT_1:def 3;
reconsider a = a as Element of J by A25;
f in dom () by ;
then ((Frege F) . f) . a = (F . a) . (f1 . a) by ;
then [p,((() . f) . a)] in the InternalRel of L by A18;
hence p <= b by ; :: thesis: verum
end;
then p <= inf (rng (() . f)) by YELLOW_0:33;
then A27: p <= Inf by YELLOW_2:def 6;
reconsider P = D --> J as ManySortedSet of D ;
reconsider R = Frege F as DoubleIndexedSet of P,L ;
reconsider f2 = f as Element of D ;
Inf in rng () by WAYBEL_5:14;
then Inf <= sup (rng ()) by YELLOW_2:22;
then Inf <= Sup by YELLOW_2:def 5;
hence p <= Sup by ; :: thesis: verum
end;
then A28: sup X <= Sup by YELLOW_0:32;
( Inf >= Sup & Inf = sup X ) by ;
hence //\ ((\// (F,L)),L) = \\/ ((/\\ ((),L)),L) by ; :: thesis: verum