:: deftheorem Def3 defines transitive ORDERS_2:def 3 :
for A being RelStr holds
( A is transitive iff the InternalRel of A is_transitive_in the carrier of A );