thus ( O is asymmetric implies the InternalRel of O is_asymmetric_in the carrier of O ) :: thesis: ( the InternalRel of O is_asymmetric_in the carrier of O implies O is asymmetric )

proof

assume the InternalRel of O is asymmetric ; :: according to NECKLACE:def 5 :: thesis: the InternalRel of O is_asymmetric_in the carrier of O
hence the InternalRel of O is_asymmetric_in the carrier of O by PARTIT_2:30; :: thesis: verum

end;

assume the InternalRel of O is_asymmetric_in the carrier of O ; :: thesis: O is asymmetric
hence the InternalRel of O is asymmetric by PARTIT_2:31; :: according to NECKLACE:def 5 :: thesis: verum