let L be non empty reflexive antisymmetric lower-bounded RelStr ; :: thesis: for x being Element of L holds Bottom L << x
let x be Element of L; :: thesis: Bottom L << x
let D be non empty directed Subset of L; :: according to WAYBEL_3:def 1 :: thesis: ( x <= sup D implies ex d being Element of L st
( d in D & Bottom L <= d ) )
assume x <= sup D ; :: thesis: ex d being Element of L st
( d in D & Bottom L <= d )
set d = the Element of D;
reconsider d = the Element of D as Element of L ;
take d ; :: thesis: ( d in D & Bottom L <= d )
thus ( d in D & Bottom L <= d ) by YELLOW_0:44; :: thesis: verum