id {{}} is_symmetric_in {{}} by PARTIT_2:23;
hence TrivOrthoRelStr is symmetric by CARD_1:49, NECKLACE:def 3; :: thesis: verum