A1: ( rng (id {{}}) = {{}} & field (id {{}}) = (dom (id {{}})) \/ (rng (id {{}})) ) by RELAT_1:71, RELAT_1:def 6;
( id {{}} is_reflexive_in field (id {{}}) & dom (id {{}}) = {{}} ) by RELAT_1:71, RELAT_2:def 9;
hence TrivOrthoRelStr is reflexive by A1, CARD_1:87, ORDERS_2:def 4; :: thesis: verum