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₁[ object , object ] means ex A being set st
( A = $2 & A c= PRIME (L ~) & $1 = "\/" (A,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 object st e in the carrier of L holds
ex u being object st S₁[e,u]

proof

let e be object ; :: thesis: ( e in the carrier of L implies ex u being object st S₁[e,u] )
assume e in the carrier of L ; :: thesis: ex u being object 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 :: thesis: for p1 being object st p1 in X holds
p1 in PRIME (L ~)

let p1 be object ; :: 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 ;
hence p1 in PRIME (L ~) by Def7; :: thesis: verum

end;

then X c= PRIME (L ~) ;
hence ex u being object 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 object 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 object ; :: 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 A11: S₁[e,f . e] by A7;
then f . e c= PRIME (L ~) ;
then A12: f . e c= the carrier of (L ~) by XBOOLE_1:1;
( e = "\/" ((f . e),L) & f . e in rng f ) by A6, FUNCT_1:def 3, A11;
hence e in { (sup X) where X is Subset of L : ( X in rng f & sup X in waybelow l ) } by A10, A12; :: thesis: verum

end;

defpred S₂[ Subset of L] means ( $1 in rng f & sup $1 in waybelow l );
A13: 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 ) } ;
A14: 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 object ; :: 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
A15: e in Y and
A16: 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
A17: Y = X and
A18: X in rng f and
A19: sup X in waybelow l by A16;
reconsider e1 = e as Element of L by A15, A17;
e1 <= sup X by A15, A17, YELLOW_2:22;
then A20: e in waybelow l by A19, WAYBEL_0:def 19;
consider r being object such that
A21: ( r in dom f & X = f . r ) by A18, FUNCT_1:def 3;
S₁[r,f . r] by A6, A7, A21;
then X c= PRIME (L ~) by A21;
hence e in (waybelow l) /\ (PRIME (L ~)) by A15, A17, A20, XBOOLE_0:def 4; :: thesis: verum

end;

A22: 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 A23: "\/" (((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 object ; :: 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 A13, 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 A22, A8, A14, YELLOW_0:34;
hence l = "\/" (((waybelow l) /\ (PRIME (L opp))),L) by A13, A23, ORDERS_2:2; :: thesis: verum