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 4 :: 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:25; :: 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:24; :: according to ORDERS_2:def 4 :: thesis: verum