let L be non empty reflexive antisymmetric RelStr ; :: 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: 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 ) ; :: according to WAYBEL_3:def 1 :: thesis: x <= y
A2: {y} is directed by WAYBEL_0:5;
sup {y} = y by YELLOW_0:39;
then ex d being Element of L st
( d in {y} & x <= d ) by A1, A2;
hence x <= y by TARSKI:def 1; :: thesis: verum