theorem Th3: :: OPOSET_1:3

TrivOrthoRelStr is reflexive