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