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

proof

assume the InternalRel of O is_antisymmetric_in the carrier of O ; :: according to ORDERS_2:def 6 :: thesis: the InternalRel of O is antisymmetric Relation of the carrier of O
hence the InternalRel of O is antisymmetric Relation of the carrier of O by PARTIT_2:27; :: thesis: verum

end;

assume the InternalRel of O is antisymmetric Relation of the carrier of O ; :: thesis: O is antisymmetric
hence the InternalRel of O is_antisymmetric_in the carrier of O by PARTIT_2:26; :: according to ORDERS_2:def 6 :: thesis: verum