field (id {{} }) = {{} } by Th1;
then id {{} } is_symmetric_in {{} } by Th9;
hence TrivOrthoRelStr is symmetric by CARD_1:87, NECKLACE:def 4; :: thesis: verum