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: 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 M19(b₁,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 M19(J,b₁,J --> the carrier of L) holds //\ (\// b₂,L),L = \\/ (/\\ (Frege b₂),L),L
let K be V11() ManySortedSet of ; :: thesis: for b₁ being M19(J,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
A2: Inf >= Sup by WAYBEL_5:16;
set l = Inf ;
set X = (waybelow (Inf )) /\ (PRIME (L ~ ));
A3: (waybelow (Inf )) /\ (PRIME (L ~ )) c= waybelow (Inf ) by XBOOLE_1:17;
reconsider X = (waybelow (Inf )) /\ (PRIME (L ~ )) as Subset of L ;
A4: Inf = sup X by A1, Th37;
A5: dom F = J by PARTFUN1:def 4;
A6: 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 by Def8; :: thesis: verum

end;

A7: inf (rng (Sups )) = 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 )
assume A8: p in X ; :: thesis: p <= Sup
defpred S₁[ set , set ] means ( $2 in K . $1 & [p,((F . $1) . $2)] in the InternalRel of L );
A9: for j being set st j in J holds
ex k being set st S₁[j,k]

proof

let j1 be set ; :: thesis: ( j1 in J implies ex k being set st S₁[j1,k] )
assume j1 in J ; :: thesis: ex k being set st S₁[j1,k]
then reconsider j = j1 as Element of J ;
A10: p << Inf by A3, A8, WAYBEL_3:7;
dom (Sups ) = J by A5, FUNCT_2:def 1;
then A11: (Sups ) . j in rng (Sups ) by FUNCT_1:def 5;
Sup = (Sups ) . j by A5, WAYBEL_5:def 1;
then A12: Inf <= Sup by A7, A11, YELLOW_2:24;
Sup = sup (rng (F . j)) by YELLOW_2:def 5;
then consider A being finite Subset of L such that
A13: ( A c= rng (F . j) & p <= sup A ) by A10, A12, WAYBEL_3:18;
consider k being Element of K . j;
( A c= A \/ {((F . j) . k)} & ex_sup_of A,L & ex_sup_of A \/ {((F . j) . k)},L ) by XBOOLE_1:7, YELLOW_0:17;
then sup A <= sup (A \/ {((F . j) . k)}) by YELLOW_0:34;
then A14: p <= sup (A \/ {((F . j) . k)}) by A13, ORDERS_2:26;
p is co-prime by A6, A8;
then consider a being Element of L such that
A15: ( a in A \/ {((F . j) . k)} & p <= a ) by A14, Th23;

per cases ( a in A or a in {((F . j) . k)} ) by A15, XBOOLE_0:def 3;

suppose a in A ; :: thesis: ex k being set st S₁[j1,k]

then consider k1 being set such that
A16: ( k1 in dom (F . j) & a = (F . j) . k1 ) by A13, FUNCT_1:def 5;
reconsider k1 = k1 as Element of K . j by A16;
[p,((F . j) . k1)] in the InternalRel of L by A15, A16, ORDERS_2:def 9;
hence ex k being set st S₁[j1,k] ; :: thesis: verum

end;

suppose a in {((F . j) . k)} ; :: thesis: ex k being set st S₁[j1,k]

then a = (F . j) . k by TARSKI:def 1;
then [p,((F . j) . k)] in the InternalRel of L by A15, ORDERS_2:def 9;
hence ex k being set st S₁[j1,k] ; :: thesis: verum

end;

end;

end;

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

now

let g be set ; :: thesis: ( g in dom f1 implies g in dom (doms F) )
assume A19: g in dom f1 ; :: thesis: g in dom (doms F)
F . g is Function ;
then g in F " (SubFuncs (rng F)) by A5, A17, A19, FUNCT_6:28;
hence g in dom (doms F) by FUNCT_6:def 2; :: thesis: verum

end;

then A20: dom f1 c= dom (doms F) by TARSKI:def 3;

now

let g be set ; :: 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 F " (SubFuncs (rng F)) by FUNCT_6:def 2;
hence g in dom f1 by A5, A17, FUNCT_6:28; :: thesis: verum

end;

then A21: dom (doms F) c= dom f1 by TARSKI:def 3;
then A22: dom f1 = dom (doms F) by A20, XBOOLE_0:def 10;
A23: for b being set st b in dom (doms F) holds
f1 . b in (doms F) . b

proof

let b be set ; :: thesis: ( b in dom (doms F) implies f1 . b in (doms F) . b )
assume A24: b in dom (doms F) ; :: thesis: f1 . b in (doms F) . b
then A25: F . b is Function of (K . b),the carrier of L by A17, A21, WAYBEL_5:6;
(doms F) . b = dom (F . b) by A5, A17, A21, A24, FUNCT_6:31
.= K . b by A25, FUNCT_2:def 1 ;
hence f1 . b in (doms F) . b by A17, A18, A21, A24; :: thesis: verum

end;

then A26: f1 in product (doms F) by A22, CARD_3:18;
reconsider f = f1 as Element of product (doms F) by A22, A23, CARD_3:18;
p is_<=_than rng ((Frege F) . f)

proof

let b be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not b in rng ((Frege F) . f) or p <= b )
assume b in rng ((Frege F) . f) ; :: thesis: p <= b
then consider a being set such that
A27: ( a in dom ((Frege F) . f) & b = ((Frege F) . f) . a ) by FUNCT_1:def 5;
reconsider a = a as Element of J by A27;
( f in dom (Frege F) & a in dom F ) by A5, A26, PARTFUN1:def 4;
then ((Frege F) . f) . a = (F . a) . (f1 . a) by WAYBEL_5:9;
then [p,(((Frege F) . f) . a)] in the InternalRel of L by A18;
hence p <= b by A27, ORDERS_2:def 9; :: thesis: verum

end;

then p <= inf (rng ((Frege F) . f)) by YELLOW_0:33;
then A28: p <= Inf by YELLOW_2:def 6;
reconsider D = product (doms F) as non empty set by A22, A23, CARD_3:18;
reconsider f2 = f as Element of D ;
reconsider P = D --> J as ManySortedSet of ;
reconsider R = Frege F as DoubleIndexedSet of P,L ;
Inf in rng (Infs ) by WAYBEL_5:14;
then Inf <= sup (rng (Infs )) by YELLOW_2:24;
then Inf <= Sup by YELLOW_2:def 5;
hence p <= Sup by A28, ORDERS_2:26; :: thesis: verum

end;

then sup X <= Sup by YELLOW_0:32;
hence //\ (\// F,L),L = \\/ (/\\ (Frege F),L),L by A2, A4, ORDERS_2:25; :: thesis: verum