( rng (id {{}}) = {{}} & field (id {{}}) = (dom (id {{}})) \/ (rng (id {{}})) ) ;
hence TrivOrthoRelStr is reflexive by CARD_1:49, ORDERS_2:def 2, RELAT_2:def 9; :: thesis: verum