let L be complete continuous LATTICE; ( ( 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 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 ) )
; 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 S1[e,u]
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 CLASSES1:sch 1(A2);
let l be Element of L; 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 ) }
defpred S2[ 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 ;
TARSKI:def 3 ( 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 ) }
;
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;
S1[
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;
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 : S2[X] } c= waybelow l
then l =
"\/" ( { (sup X) where X is Subset of L : S2[X] } ,L)
by A13, A9, XBOOLE_0:def 10
.=
"\/" ((union { X where X is Subset of L : S2[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; verum