:: deftheorem defines is_way_below WAYBEL_3:def 1 :
for L being non empty reflexive RelStr
for x, y being Element of L holds
( x is_way_below y iff 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 ) );