theorem Th7: :: WAYBEL_3:7

for L being non empty reflexive RelStr
for x, y being Element of L holds
( x in waybelow y iff x << y )