let L be lower-bounded continuous LATTICE; :: thesis:
let x, y be Element of L; :: thesis:

hereby :: thesis:

assume A1: x << y ; :: thesis:
let D be non empty directed Subset of L; :: thesis:
assume A2: y <= sup D ; :: thesis:
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:

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:
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:
assume y <= sup D ; :: thesis:
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:

end;

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