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_{1} being set

for b_{2} being set

for b_{3} being ManySortedFunction of b_{2},b_{1} --> the carrier of L holds //\ ((\// (b_{3},L)),L) = \\/ ((/\\ ((Frege b_{3}),L)),L)

let J be non empty set ; :: thesis: for b_{1} being set

for b_{2} being ManySortedFunction of b_{1},J --> the carrier of L holds //\ ((\// (b_{2},L)),L) = \\/ ((/\\ ((Frege b_{2}),L)),L)

let K be V11() ManySortedSet of J; :: thesis: for b_{1} being ManySortedFunction of K,J --> the carrier of L holds //\ ((\// (b_{1},L)),L) = \\/ ((/\\ ((Frege b_{1}),L)),L)

let F be DoubleIndexedSet of K,L; :: thesis: //\ ((\// (F,L)),L) = \\/ ((/\\ ((Frege F),L)),L)

set l = Inf ;

set X = (waybelow (Inf )) /\ (PRIME (L ~));

A2: (waybelow (Inf )) /\ (PRIME (L ~)) c= waybelow (Inf ) by XBOOLE_1:17;

reconsider X = (waybelow (Inf )) /\ (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

X is_<=_than Sup

( Inf >= Sup & Inf = sup X ) by A1, Th37, WAYBEL_5:16;

hence //\ ((\// (F,L)),L) = \\/ ((/\\ ((Frege F),L)),L) by A28, ORDERS_2:2; :: thesis: verum

( 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

for b

for b

let J be non empty set ; :: thesis: for b

for b

let K be V11() ManySortedSet of J; :: thesis: for b

let F be DoubleIndexedSet of K,L; :: thesis: //\ ((\// (F,L)),L) = \\/ ((/\\ ((Frege F),L)),L)

set l = Inf ;

set X = (waybelow (Inf )) /\ (PRIME (L ~));

A2: (waybelow (Inf )) /\ (PRIME (L ~)) c= waybelow (Inf ) by XBOOLE_1:17;

reconsider X = (waybelow (Inf )) /\ (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

A5:
inf (rng (Sups )) = Inf
by YELLOW_2:def 6;
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;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

X is_<=_than Sup

proof

then A28:
sup X <= Sup
by YELLOW_0:32;
let p be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not p in X or p <= Sup )

defpred S_{1}[ object , object ] means ( $2 in K . $1 & [p,((F . $1) . $2)] in the InternalRel of L );

assume A6: p in X ; :: thesis: p <= Sup

A7: for j being object st j in J holds

ex k being object st S_{1}[j,k]

A17: dom f1 = J and

A18: for j being object st j in J holds

S_{1}[j,f1 . j]
from CLASSES1:sch 1(A7);

for g being object st g in dom f1 holds

g in dom (doms F) by FUNCT_6:def 2, A3, A17;

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

reconsider f = f1 as Element of product (doms F) by A20, A21, CARD_3:9;

A24: f1 in product (doms F) by A20, A21, CARD_3:9;

p is_<=_than rng ((Frege F) . f)

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 (Infs ) by WAYBEL_5:14;

then Inf <= sup (rng (Infs )) by YELLOW_2:22;

then Inf <= Sup by YELLOW_2:def 5;

hence p <= Sup by A27, ORDERS_2:3; :: thesis: verum

end;defpred S

assume A6: p in X ; :: thesis: p <= Sup

A7: for j being object st j in J holds

ex k being object st S

proof

consider f1 being Function such that
let j1 be object ; :: thesis: ( j1 in J implies ex k being object st S_{1}[j1,k] )

assume j1 in J ; :: thesis: ex k being object st S_{1}[j1,k]

then reconsider j = j1 as Element of J ;

set k = the Element of K . j;

dom (Sups ) = J by A3, FUNCT_2:def 1;

then A8: (Sups ) . j in rng (Sups ) by FUNCT_1:def 3;

A9: ( p << Inf & Sup = sup (rng (F . j)) ) by A2, A6, WAYBEL_3:7, YELLOW_2:def 5;

Sup = (Sups ) . j by A3, WAYBEL_5:def 1;

then Inf <= Sup by A5, A8, YELLOW_2:22;

then consider A being finite Subset of L such that

A10: A c= rng (F . j) and

A11: p <= sup A by A9, WAYBEL_3:18;

( 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 XBOOLE_1:7, YELLOW_0:34;

then A12: p <= sup (A \/ {((F . j) . the Element of K . j)}) by A11, ORDERS_2:3;

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 A12, Th23;

end;assume j1 in J ; :: thesis: ex k being object st S

then reconsider j = j1 as Element of J ;

set k = the Element of K . j;

dom (Sups ) = J by A3, FUNCT_2:def 1;

then A8: (Sups ) . j in rng (Sups ) by FUNCT_1:def 3;

A9: ( p << Inf & Sup = sup (rng (F . j)) ) by A2, A6, WAYBEL_3:7, YELLOW_2:def 5;

Sup = (Sups ) . j by A3, WAYBEL_5:def 1;

then Inf <= Sup by A5, A8, YELLOW_2:22;

then consider A being finite Subset of L such that

A10: A c= rng (F . j) and

A11: p <= sup A by A9, WAYBEL_3:18;

( 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 XBOOLE_1:7, YELLOW_0:34;

then A12: p <= sup (A \/ {((F . j) . the Element of K . j)}) by A11, ORDERS_2:3;

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 A12, Th23;

per cases
( a in A or a in {((F . j) . the Element of K . j)} )
by A13, XBOOLE_0:def 3;

end;

suppose
a in A
; :: thesis: ex k being object st S_{1}[j1,k]

then consider k1 being object such that

A15: k1 in dom (F . j) and

A16: a = (F . j) . k1 by A10, FUNCT_1:def 3;

reconsider k1 = k1 as Element of K . j by A15;

[p,((F . j) . k1)] in the InternalRel of L by A14, A16, ORDERS_2:def 5;

hence ex k being object st S_{1}[j1,k]
; :: thesis: verum

end;A15: k1 in dom (F . j) and

A16: a = (F . j) . k1 by A10, FUNCT_1:def 3;

reconsider k1 = k1 as Element of K . j by A15;

[p,((F . j) . k1)] in the InternalRel of L by A14, A16, ORDERS_2:def 5;

hence ex k being object st S

A17: dom f1 = J and

A18: for j being object st j in J holds

S

now :: thesis: for g being object st g in dom (doms F) holds

g in dom f1

then A19:
dom (doms F) c= dom f1
;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;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

for g being object st g in dom f1 holds

g in dom (doms F) by FUNCT_6:def 2, A3, A17;

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

then reconsider D = product (doms F) as non empty set by A20, CARD_3:9;
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 A17, A19, WAYBEL_5:6;

(doms F) . b = dom (F . b) by A3, A17, A19, A22, FUNCT_6:22

.= K . b by A23, FUNCT_2:def 1 ;

hence f1 . b in (doms F) . b by A17, A18, A19, A22; :: thesis: verum

end;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 A17, A19, WAYBEL_5:6;

(doms F) . b = dom (F . b) by A3, A17, A19, A22, FUNCT_6:22

.= K . b by A23, FUNCT_2:def 1 ;

hence f1 . b in (doms F) . b by A17, A18, A19, A22; :: thesis: verum

reconsider f = f1 as Element of product (doms F) by A20, A21, CARD_3:9;

A24: f1 in product (doms F) by A20, A21, CARD_3:9;

p is_<=_than rng ((Frege F) . f)

proof

then
p <= inf (rng ((Frege F) . f))
by YELLOW_0:33;
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 object such that

A25: a in dom ((Frege F) . f) and

A26: b = ((Frege F) . f) . a by FUNCT_1:def 3;

reconsider a = a as Element of J by A25;

f in dom (Frege F) by A24, PARTFUN1:def 2;

then ((Frege F) . f) . a = (F . a) . (f1 . a) by A3, WAYBEL_5:9;

then [p,(((Frege F) . f) . a)] in the InternalRel of L by A18;

hence p <= b by A26, ORDERS_2:def 5; :: thesis: verum

end;assume b in rng ((Frege F) . f) ; :: thesis: p <= b

then consider a being object such that

A25: a in dom ((Frege F) . f) and

A26: b = ((Frege F) . f) . a by FUNCT_1:def 3;

reconsider a = a as Element of J by A25;

f in dom (Frege F) by A24, PARTFUN1:def 2;

then ((Frege F) . f) . a = (F . a) . (f1 . a) by A3, WAYBEL_5:9;

then [p,(((Frege F) . f) . a)] in the InternalRel of L by A18;

hence p <= b by A26, ORDERS_2:def 5; :: thesis: verum

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 (Infs ) by WAYBEL_5:14;

then Inf <= sup (rng (Infs )) by YELLOW_2:22;

then Inf <= Sup by YELLOW_2:def 5;

hence p <= Sup by A27, ORDERS_2:3; :: thesis: verum

( Inf >= Sup & Inf = sup X ) by A1, Th37, WAYBEL_5:16;

hence //\ ((\// (F,L)),L) = \\/ ((/\\ ((Frege F),L)),L) by A28, ORDERS_2:2; :: thesis: verum