theorem :: WAYBEL_3:10

for L being non empty reflexive antisymmetric RelStr
for x being Element of L holds x is_<=_than wayabove x by Th8, Th1;