theorem Th4: :: OPOSET_1:4

TrivAsymOrthoRelStr is irreflexive ;