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