let L be up-complete Chain; :: thesis: for x, y being Element of L st x < y holds
x << y
let x, y be Element of L; :: thesis: ( x < y implies x << y )
assume A1: ( x <= y & x <> y ) ; :: according to ORDERS_2:def 10 :: 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 that
A2: y <= sup D and
A3: for d being Element of L st d in D holds
not x <= d ; :: thesis: contradiction
A4: ex_sup_of D,L by WAYBEL_0:75;
x is_>=_than D

proof

let z be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not z in D or z <= x )
assume z in D ; :: thesis: z <= x
then not x <= z by A3;
hence z <= x by WAYBEL_0:def 29; :: thesis: verum

end;

then x >= sup D by A4, YELLOW_0:def 9;
then x >= y by A2, ORDERS_2:26;
hence contradiction by A1, ORDERS_2:25; :: thesis: verum