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