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 that
A1: x <= y and
A2: x <> y ; :: according to ORDERS_2:def 6 :: 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
A3: y <= sup D and
A4: for d being Element of L st d in D holds
not x <= d ; :: thesis: contradiction
A5: 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 A4;
hence z <= x by WAYBEL_0:def 29; :: thesis: verum
end;
then x >= sup D by A5, YELLOW_0:def 9;
then x >= y by A3, ORDERS_2:3;
hence contradiction by A1, A2, ORDERS_2:2; :: thesis: verum