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