let O be non empty RelStr ; :: thesis: ( O is reflexive & O is SubTransitive implies O is transitive )
assume A1: ( O is reflexive & O is SubTransitive ) ; :: thesis: O is transitive
set IntRel = the InternalRel of O;
set CO = the carrier of O;
A2: the InternalRel of O is_reflexive_in the carrier of O by A1, ORDERS_2:def 4;
A3: the InternalRel of O is transitive by A1, Def19;
the carrier of O = field the InternalRel of O by A2, Th7;
then the InternalRel of O is_transitive_in the carrier of O by A3, Th12;
hence O is transitive by ORDERS_2:def 5; :: thesis: verum