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