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 = "\/" ((() /\ (PRIME (L opp))),L) )

defpred S1[ 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 = "\/" ((() /\ (PRIME (L opp))),L)
A2: for e being object st e in the carrier of L holds
ex u being object st S1[e,u]
proof
let e be object ; :: thesis: ( e in the carrier of L implies ex u being object st S1[e,u] )
assume e in the carrier of L ; :: thesis: ex u being object st S1[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 S1[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
S1[e,f . e] from let l be Element of L; :: thesis: l = "\/" ((() /\ (PRIME (L opp))),L)
A8: ex_sup_of () /\ (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: S1[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 ;
hence e in { (sup X) where X is Subset of L : ( X in rng f & sup X in waybelow l ) } by ; :: thesis: verum
end;
defpred S2[ Subset of L] means ( \$1 in rng f & sup \$1 in waybelow l );
A13: l = sup () 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= () /\ (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 () /\ (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 () /\ (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 ;
e1 <= sup X by ;
then A20: e in waybelow l by ;
consider r being object such that
A21: ( r in dom f & X = f . r ) by ;
S1[r,f . r] by A6, A7, A21;
then X c= PRIME (L ~) by A21;
hence e in () /\ (PRIME (L ~)) by ; :: 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: "\/" ((() /\ (PRIME (L ~))),L) <= "\/" ((),L) by ;
{ (sup X) where X is Subset of L : S2[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 : S2[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:
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 : S2[X] } ,L) by
.= "\/" ((union { X where X is Subset of L : S2[X] } ),L) from ;
then l <= "\/" ((() /\ (PRIME (L ~))),L) by ;
hence l = "\/" ((() /\ (PRIME (L opp))),L) by ; :: thesis: verum