let L be complete LATTICE; for x, y being Element of L st x << y holds
for X being Subset of L st y <= sup X holds
ex A being finite Subset of L st
( A c= X & x <= sup A )
let x, y be Element of L; ( x << y implies for X being Subset of L st y <= sup X holds
ex A being finite Subset of L st
( A c= X & x <= sup A ) )
assume A1:
x << y
; for X being Subset of L st y <= sup X holds
ex A being finite Subset of L st
( A c= X & x <= sup A )
let X be Subset of L; ( y <= sup X implies ex A being finite Subset of L st
( A c= X & x <= sup A ) )
assume A2:
y <= sup X
; ex A being finite Subset of L st
( A c= X & x <= sup A )
defpred S1[ set ] means ex Y being finite Subset of X st
( ex_sup_of Y,L & $1 = "\/" (Y,L) );
consider F being Subset of L such that
A3:
for a being Element of L holds
( a in F iff S1[a] )
from SUBSET_1:sch 3();
A4:
for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F
by A3, YELLOW_0:17;
A5:
for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L
by YELLOW_0:17;
A6:
{} c= X
;
ex_sup_of {} ,L
by YELLOW_0:17;
then
"\/" ({},L) in F
by A3, A6;
then reconsider F = F as non empty directed Subset of L by A3, A4, A5, WAYBEL_0:51;
ex_sup_of X,L
by YELLOW_0:17;
then
sup X = sup F
by A3, A4, A5, WAYBEL_0:54;
then consider d being Element of L such that
A7:
d in F
and
A8:
x <= d
by A1, A2;
consider Y being finite Subset of X such that
ex_sup_of Y,L
and
A9:
d = "\/" (Y,L)
by A3, A7;
reconsider Y = Y as finite Subset of L by XBOOLE_1:1;
take
Y
; ( Y c= X & x <= sup Y )
thus
( Y c= X & x <= sup Y )
by A8, A9; verum