theorem Th15: :: OPOSET_1:15

TrivOrthoRelStr is QuasiOrthocomplemented