id {{} } is_symmetric_in {{} } by PARTIT_2:25;
hence TrivOrthoRelStr is symmetric by CARD_1:87, NECKLACE:def 4; :: thesis: verum