theorem Th5: :: OPOSET_1:5

TrivOrthoRelStr is symmetric ;