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