thus the carrier of TrivOrthoRelStr is 1 -element by CARD_1:49; :: according to STRUCT_0:def 19 :: thesis: verum