theorem Th3: :: ORDERS_2:3

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