theorem Th5: :: ORDERS_2:5

for A being transitive antisymmetric RelStr
for a1, a2, a3 being Element of A st a1 < a2 & a2 < a3 holds
a1 < a3 by Th3, Th4;