let L be lower-bounded continuous LATTICE; :: thesis: for x, y being Element of L holds
( x << y iff for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x << d ) )
let x, y be Element of L; :: thesis: ( x << y iff for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x << d ) )

hereby :: thesis: ( ( for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x << d ) ) implies x << y )

assume A1: x << y ; :: thesis: for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x << d )
let D be non empty directed Subset of L; :: 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 )
consider x' being Element of L such that
A3: ( x << x' & x' << y ) by A1, Th53;
consider d being Element of L such that
A4: ( d in D & x' <= d ) by A2, A3, WAYBEL_3:def 1;
thus ex d being Element of L st
( d in D & x << d ) by A3, A4, WAYBEL_3:2; :: thesis: verum

end;

assume A5: for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x << d ) ; :: thesis: x << y
for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x <= d )

proof

let D be non empty directed Subset of L; :: 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 d being Element of L such that
A6: ( d in D & x << d ) by A5;
thus ex d being Element of L st
( d in D & x <= d ) by A6, WAYBEL_3:1; :: thesis: verum

end;

hence x << y by WAYBEL_3:def 1; :: thesis: verum