thus ( O is transitive implies the InternalRel of O is transitive Relation of the carrier of O ) :: thesis: ( the InternalRel of O is transitive Relation of the carrier of O implies O is transitive )

proof

assume the InternalRel of O is_transitive_in the carrier of O ; :: according to ORDERS_2:def 3 :: thesis: the InternalRel of O is transitive Relation of the carrier of O
hence the InternalRel of O is transitive Relation of the carrier of O by PARTIT_2:27; :: thesis: verum

end;

assume the InternalRel of O is transitive Relation of the carrier of O ; :: thesis: O is transitive
hence the InternalRel of O is_transitive_in the carrier of O by PARTIT_2:26; :: according to ORDERS_2:def 3 :: thesis: verum