:: deftheorem defines waybelow WAYBEL_3:def 3 :
for L being non empty reflexive RelStr
for x being Element of L holds waybelow x = { y where y is Element of L : y << x } ;