theorem Th5: :: WAYBEL28:5

for N being non empty directed RelStr
for x, y being Element of N ex z being Element of N st
( x <= z & y <= z )