let O be non empty RelStr ; :: thesis: ( O is irreflexive & O is SubTransitive implies O is transitive )
assume A1: ( O is irreflexive & O is SubTransitive ) ; :: thesis: O is transitive
set IntRel = the InternalRel of O;
set CO = the carrier of O;
A2: field the InternalRel of O c= the carrier of O \/ the carrier of O by RELSET_1:19;
the InternalRel of O is transitive by A1, Def19;
then the InternalRel of O is_transitive_in the carrier of O by A2, Th12;
hence O is transitive by ORDERS_2:def 5; :: thesis: verum