theorem Th9: :: WAYBEL_3:9

for L being non empty reflexive antisymmetric RelStr
for x being Element of L holds x is_>=_than waybelow x by Th7, Th1;