let L be complete LATTICE; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( y <= sup X implies ex A being finite Subset of L st
( A c= X & x <= sup A ) )
assume A2: y <= sup X ; :: thesis: ex A being finite Subset of L st
( A c= X & x <= sup A )
defpred S₁[ 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 S₁[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 ; :: thesis: ( Y c= X & x <= sup Y )
thus ( Y c= X & x <= sup Y ) by A8, A9; :: thesis: verum