set R = the InternalRel of A;
( field the InternalRel of A = the carrier of A & the InternalRel of A is_transitive_in the carrier of A ) by Def5, ORDERS_1:97;
hence the InternalRel of A is transitive by RELAT_2:def 16; :: thesis: verum