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