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 )
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
let l be Element of L; :: thesis: l = "\/" ((waybelow l) /\ (PRIME (L opp ))),L
defpred S₁[ set , set ] means ( $2 c= PRIME (L ~ ) & $1 = "\/" $2,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 & ( 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 A4: p1 in X ; :: thesis: p1 in PRIME (L ~ )
then reconsider p = p1 as Element of L ;
p is co-prime by A3, A4;
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
A5: dom f = the carrier of L and
A6: for e being set st e in the carrier of L holds
S₁[e,f . e] from CLASSES1:sch 1(A2);
A7: l = sup (waybelow l) by WAYBEL_3:def 5;
A8: 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 A9: 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 A10: ( e = "\/" (f . e),L & e is Element of L ) by A6;
A11: f . e in rng f by A5, A9, FUNCT_1:def 5;
f . e c= PRIME (L ~ ) by A6, A9;
then f . e c= the carrier of (L ~ ) by XBOOLE_1:1;
hence e in { (sup X) where X is Subset of L : ( X in rng f & sup X in waybelow l ) } by A9, A10, A11; :: thesis: verum

end;

defpred S₂[ Subset of L] means ( $1 in rng f & sup $1 in waybelow l );
{ (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 consider X being Subset of L such that
A12: ( e = sup X & X in rng f & sup X in waybelow l ) ;
thus e in waybelow l by A12; :: thesis: verum

end;

then A13: l = "\/" { (sup X) where X is Subset of L : S₂[X] } ,L by A7, A8, XBOOLE_0:def 10
.= "\/" (union { X where X is Subset of L : S₂[X] } ),L from YELLOW_3:sch 5() ;
set Z = union { X where X is Subset of L : ( X in rng f & sup X in waybelow l ) } ;
A14: 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;
A15: ex_sup_of (waybelow l) /\ (PRIME (L ~ )),L by YELLOW_0:17;
A16: ex_sup_of waybelow l,L by YELLOW_0:17;
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
A17: ( e in Y & 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
A18: ( Y = X & X in rng f & sup X in waybelow l ) by A17;
consider r being set such that
A19: ( r in dom f & X = f . r ) by A18, FUNCT_1:def 5;
A20: X c= PRIME (L ~ ) by A5, A6, A19;
reconsider e1 = e as Element of L by A17, A18;
e1 <= sup X by A17, A18, YELLOW_2:24;
then e in waybelow l by A18, WAYBEL_0:def 19;
hence e in (waybelow l) /\ (PRIME (L ~ )) by A17, A18, A20, XBOOLE_0:def 4; :: thesis: verum

end;

then A21: l <= "\/" ((waybelow l) /\ (PRIME (L ~ ))),L by A13, A14, A15, YELLOW_0:34;
"\/" ((waybelow l) /\ (PRIME (L ~ ))),L <= "\/" (waybelow l),L by A15, A16, XBOOLE_1:17, YELLOW_0:34;
hence l = "\/" ((waybelow l) /\ (PRIME (L opp ))),L by A7, A21, ORDERS_2:25; :: thesis: verum