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

proof

assume the InternalRel of O is_symmetric_in the carrier of O ; :: according to NECKLACE:def 3 :: thesis: the InternalRel of O is symmetric Relation of the carrier of O
hence the InternalRel of O is symmetric Relation of the carrier of O by PARTIT_2:22; :: thesis: verum

end;

assume the InternalRel of O is symmetric Relation of the carrier of O ; :: thesis: O is symmetric
hence the InternalRel of O is_symmetric_in the carrier of O by PARTIT_2:23; :: according to NECKLACE:def 3 :: thesis: verum