theorem Th6: :: ORDERS_2:6

for A being antisymmetric RelStr
for a1, a2 being Element of A st a1 <= a2 holds
not a2 < a1 by Th2;