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