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 x9 being Element of L such that
A3: x << x9 and
A4: x9 << y by A1, Th52;
ex d being Element of L st
( d in D & x9 <= d ) by A2, A4, WAYBEL_3:def 1;
hence ex d being Element of L st
( d in D & x << d ) by A3, 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 ex d being Element of L st
( d in D & x << d ) by A5;
hence ex d being Element of L st
( d in D & x <= d ) by WAYBEL_3:1; :: thesis: verum

end;

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