for A being transitive RelStr
for a1, a2, a3 being Element of A holds
( ( a1 <~ a2 & a2 <= a3 implies a1 <~ a3 ) & ( a1 <= a2 & a2 <~ a3 implies a1 <~ a3 ) ) by ORDERS_2:3;