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

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

assume A1: x << y ; :: thesis: for D being non empty directed Subset of st y <= sup D holds
ex d being Element of st
( d in D & x << d )
let D be non empty directed Subset of ; :: thesis: ( y <= sup D implies ex d being Element of st
( d in D & x << d ) )
assume A2: y <= sup D ; :: thesis: ex d being Element of st
( d in D & x << d )
consider x' being Element of such that
A3: x << x' and
A4: x' << y by A1, Th53;
ex d being Element of st
( d in D & x' <= d ) by A2, A4, WAYBEL_3:def 1;
hence ex d being Element of st
( d in D & x << d ) by A3, WAYBEL_3:2; :: thesis: verum

end;

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

proof

let D be non empty directed Subset of ; :: thesis: ( y <= sup D implies ex d being Element of st
( d in D & x <= d ) )
assume y <= sup D ; :: thesis: ex d being Element of st
( d in D & x <= d )
then ex d being Element of st
( d in D & x << d ) by A5;
hence ex d being Element of st
( d in D & x <= d ) by WAYBEL_3:1; :: thesis: verum

end;

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