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
( {y} is directed & sup {y} = y & y <= y ) by WAYBEL_0:5, YELLOW_0:39;
then consider d being Element of L such that
A2: ( d in {y} & x <= d ) by A1;
thus x <= y by A2, TARSKI:def 1; :: thesis: verum