theorem Th8: :: WAYBEL_3:8

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