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_{1}[ 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_{1}[e,u]

A6: dom f = the carrier of L and

A7: for e being object st e in the carrier of L holds

S_{1}[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 ) }_{2}[ 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 ~))

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_{2}[X] } c= waybelow l
_{2}[X] } ,L)
by A13, A9, XBOOLE_0:def 10

.= "\/" ((union { X where X is Subset of L : S_{2}[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

( 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

( 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

proof

consider f being Function such that
let e be object ; :: thesis: ( e in the carrier of L implies ex u being object st S_{1}[e,u] )

assume e in the carrier of L ; :: thesis: ex u being object st S_{1}[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;

hence ex u being object st S_{1}[e,u]
by A3; :: thesis: verum

end;assume e in the carrier of L ; :: thesis: ex u being object st S

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 ~)

then
X c= PRIME (L ~)
;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;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

hence ex u being object st S

A6: dom f = the carrier of L and

A7: for e being object st e in the carrier of L holds

S

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

defpred S
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_{1}[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;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

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

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

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;
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_{1}[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;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

then X c= PRIME (L ~) by A21;

hence e in (waybelow l) /\ (PRIME (L ~)) by A15, A17, A20, XBOOLE_0:def 4; :: thesis: verum

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

proof

then l =
"\/" ( { (sup X) where X is Subset of L : S
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (sup X) where X is Subset of L : S_{2}[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;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

.= "\/" ((union { X where X is Subset of L : S

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