for x being set st x in {{}} holds
not [x,x] in {} ({{}},{{}}) ;
hence TrivAsymOrthoRelStr is irreflexive by Def6, CARD_1:49, RELAT_2:def 2; :: thesis: verum