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