:: deftheorem Def1 defines -waybelow WAYBEL_4:def 1 :
for L being non empty reflexive RelStr
for b₂ being Relation of L holds
( b₂ = L -waybelow iff for x, y being Element of L holds
( [x,y] in b₂ iff x << y ) );