let O be non empty RelStr ; :: thesis: ( O is reflexive & O is SubSymmetric implies O is symmetric )
set IntRel = the InternalRel of O;
set CO = the carrier of O;
assume ( O is reflexive & O is SubSymmetric ) ; :: thesis: O is symmetric
then the InternalRel of O is symmetric by Def13;
then the InternalRel of O is_symmetric_in the carrier of O by Th9;
hence O is symmetric by NECKLACE:def 4; :: thesis: verum