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 for l being Element of L holds l = "\/" (((waybelow l) /\ (PRIME (L opp))),L) )
defpred S₁[ set , set ] means ( $2 c= PRIME (L ~) & $1 = "\/" ($2,L) );
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: for l being Element of L holds l = "\/" (((waybelow l) /\ (PRIME (L opp))),L)
A2: for e being set st e in the carrier of L holds
ex u being set st S₁[e,u]

proof

let e be set ; :: thesis: ( e in the carrier of L implies ex u being set st S₁[e,u] )
assume e in the carrier of L ; :: thesis: ex u being set st S₁[e,u]
then reconsider l = e as Element of L ;
consider X being Subset of L such that
A3: l = sup X and
A4: for x being Element of L st x in X holds
x is co-prime by A1;

now

let p1 be set ; :: thesis: ( p1 in X implies p1 in PRIME (L ~) )
assume A5: p1 in X ; :: thesis: p1 in PRIME (L ~)
then reconsider p = p1 as Element of L ;
p is co-prime by A4, A5;
then p ~ is prime by Def8;
hence p1 in PRIME (L ~) by Def7; :: thesis: verum

end;

then X c= PRIME (L ~) by TARSKI:def 3;
hence ex u being set st S₁[e,u] by A3; :: thesis: verum

end;

consider f being Function such that
A6: dom f = the carrier of L and
A7: for e being set st e in the carrier of L holds
S₁[e,f . e] from CLASSES1:sch 1(A2);
let l be Element of L; :: thesis: l = "\/" (((waybelow l) /\ (PRIME (L opp))),L)
A8: ex_sup_of (waybelow l) /\ (PRIME (L ~)),L by YELLOW_0:17;
A9: waybelow l c= { (sup X) where X is Subset of L : ( X in rng f & sup X in waybelow l ) }

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in waybelow l or e in { (sup X) where X is Subset of L : ( X in rng f & sup X in waybelow l ) } )
assume A10: e in waybelow l ; :: thesis: e in { (sup X) where X is Subset of L : ( X in rng f & sup X in waybelow l ) }
then f . e c= PRIME (L ~) by A7;
then A11: f . e c= the carrier of (L ~) by XBOOLE_1:1;
( e = "\/" ((f . e),L) & f . e in rng f ) by A6, A7, A10, FUNCT_1:def 3;
hence e in { (sup X) where X is Subset of L : ( X in rng f & sup X in waybelow l ) } by A10, A11; :: thesis: verum

end;

defpred S₂[ Subset of L] means ( $1 in rng f & sup $1 in waybelow l );
A12: l = sup (waybelow l) by WAYBEL_3:def 5;
set Z = union { X where X is Subset of L : ( X in rng f & sup X in waybelow l ) } ;
A13: union { X where X is Subset of L : ( X in rng f & sup X in waybelow l ) } c= (waybelow l) /\ (PRIME (L ~))

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in union { X where X is Subset of L : ( X in rng f & sup X in waybelow l ) } or e in (waybelow l) /\ (PRIME (L ~)) )
assume e in union { X where X is Subset of L : ( X in rng f & sup X in waybelow l ) } ; :: thesis: e in (waybelow l) /\ (PRIME (L ~))
then consider Y being set such that
A14: e in Y and
A15: Y in { X where X is Subset of L : ( X in rng f & sup X in waybelow l ) } by TARSKI:def 4;
consider X being Subset of L such that
A16: Y = X and
A17: X in rng f and
A18: sup X in waybelow l by A15;
reconsider e1 = e as Element of L by A14, A16;
e1 <= sup X by A14, A16, YELLOW_2:22;
then A19: e in waybelow l by A18, WAYBEL_0:def 19;
ex r being set st
( r in dom f & X = f . r ) by A17, FUNCT_1:def 3;
then X c= PRIME (L ~) by A6, A7;
hence e in (waybelow l) /\ (PRIME (L ~)) by A14, A16, A19, XBOOLE_0:def 4; :: thesis: verum

end;

A20: ex_sup_of union { X where X is Subset of L : ( X in rng f & sup X in waybelow l ) } ,L by YELLOW_0:17;
ex_sup_of waybelow l,L by YELLOW_0:17;
then A21: "\/" (((waybelow l) /\ (PRIME (L ~))),L) <= "\/" ((waybelow l),L) by A8, XBOOLE_1:17, YELLOW_0:34;
{ (sup X) where X is Subset of L : S₂[X] } c= waybelow l

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (sup X) where X is Subset of L : S₂[X] } or e in waybelow l )
assume e in { (sup X) where X is Subset of L : ( X in rng f & sup X in waybelow l ) } ; :: thesis: e in waybelow l
then ex X being Subset of L st
( e = sup X & X in rng f & sup X in waybelow l ) ;
hence e in waybelow l ; :: thesis: verum

end;

then l = "\/" ( { (sup X) where X is Subset of L : S₂[X] } ,L) by A12, A9, XBOOLE_0:def 10
.= "\/" ((union { X where X is Subset of L : S₂[X] } ),L) from YELLOW_3:sch 5() ;
then l <= "\/" (((waybelow l) /\ (PRIME (L ~))),L) by A20, A8, A13, YELLOW_0:34;
hence l = "\/" (((waybelow l) /\ (PRIME (L opp))),L) by A12, A21, ORDERS_2:2; :: thesis: verum