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