theorem Th2: :: ORDERS_2:2

for A being antisymmetric RelStr
for a1, a2 being Element of A st a1 <= a2 & a2 <= a1 holds
a1 = a2