theorem Th4: :: ORDERS_2:4

for A being antisymmetric RelStr
for a1, a2 being Element of A holds
( not a1 < a2 or not a2 < a1 ) by Th2;