theorem Th1: :: WAYBEL_3:1

for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st x << y holds
x <= y