let L be non empty up-complete Poset; :: thesis: for x, y being Element of L st ( for I being Ideal of L st y <= sup I holds
x in I ) holds
x << y
let x, y be Element of L; :: thesis: ( ( for I being Ideal of L st y <= sup I holds
x in I ) implies x << y )
assume A1: for I being Ideal of L st y <= sup I holds
x in I ; :: 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 A2: y <= sup D ; :: thesis: ex d being Element of L st
( d in D & x <= d )
ex_sup_of D,L by WAYBEL_0:75;
then sup D = sup (downarrow D) by WAYBEL_0:33;
then x in downarrow D by A1, A2;
then ex d being Element of L st
( x <= d & d in D ) by WAYBEL_0:def 15;
hence ex d being Element of L st
( d in D & x <= d ) ; :: thesis: verum