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: now

let Y be finite Subset of X; :: thesis: ( Y <> {} implies "\/" Y,L in F )
assume Y <> {} ; :: thesis: "\/" Y,L in F
ex_sup_of Y,L by YELLOW_0:17;
hence "\/" Y,L in F by A3; :: thesis: verum

end;

A5: for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L by YELLOW_0:17;
( {} c= X & ex_sup_of {} ,L ) by XBOOLE_1:2, YELLOW_0:17;
then "\/" {} ,L in F by A3;
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
A6: ( d in F & x <= d ) by A1, A2, Def1;
consider Y being finite Subset of X such that
A7: ( ex_sup_of Y,L & d = "\/" Y,L ) by A3, A6;
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 A6, A7; :: thesis: verum