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