let L be complete LATTICE; :: thesis: for x, y being Element of L st ( 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 ) ) holds
x << y
let x, y be Element of L; :: 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 ) ) implies x << y )
assume A1: 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 ) ; :: thesis: x << y
let D be non empty directed Subset of L; :: according to WAYBEL_3:def 1 :: thesis: ( y <= sup D implies ex d being Element of L st
( d in D & x <= d ) )
assume y <= sup D ; :: thesis: ex d being Element of L st
( d in D & x <= d )
then consider A being finite Subset of L such that
A2: A c= D and
A3: x <= sup A by A1;
reconsider B = A as finite Subset of D by A2;
consider a being Element of L such that
A4: a in D and
A5: a is_>=_than B by WAYBEL_0:1;
take a ; :: thesis: ( a in D & x <= a )
a >= sup A by A5, YELLOW_0:32;
hence ( a in D & x <= a ) by A3, A4, YELLOW_0:def 2; :: thesis: verum