theorem Th17: :: OPOSET_1:17

TrivOrthoRelStr is Orthocomplemented