let L be complete LATTICE; :: thesis: for x, y being Element of st x << y holds
for X being Subset of st y <= sup X holds
ex A being finite Subset of st
( A c= X & x <= sup A )
let x, y be Element of ; :: thesis: ( x << y implies for X being Subset of st y <= sup X holds
ex A being finite Subset of st
( A c= X & x <= sup A ) )
assume A1: x << y ; :: thesis: for X being Subset of st y <= sup X holds
ex A being finite Subset of st
( A c= X & x <= sup A )
let X be Subset of ; :: thesis: ( y <= sup X implies ex A being finite Subset of st
( A c= X & x <= sup A ) )
assume A2: y <= sup X ; :: thesis: ex A being finite Subset of st
( A c= X & x <= sup A )
defpred S₁[ set ] means ex Y being finite Subset of st
( ex_sup_of Y,L & $1 = "\/" Y,L );
consider F being Subset of such that
A3: for a being Element of holds
( a in F iff S₁[a] ) from SUBSET_1:sch 3();

A4: now

let Y be finite Subset of ; :: 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 st Y <> {} holds
ex_sup_of Y,L by YELLOW_0:17;
A6: {} c= X by XBOOLE_1:2;
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 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 such that
A7: d in F and
A8: x <= d by A1, A2, Def1;
consider Y being finite Subset of such that
ex_sup_of Y,L and
A9: d = "\/" Y,L by A3, A7;
reconsider Y = Y as finite Subset of 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