take TrivOrthoRelStr ; :: thesis: ( TrivOrthoRelStr is Orthocomplemented & TrivOrthoRelStr is QuasiOrthocomplemented & TrivOrthoRelStr is PartialOrdered )
thus ( TrivOrthoRelStr is Orthocomplemented & TrivOrthoRelStr is QuasiOrthocomplemented & TrivOrthoRelStr is PartialOrdered ) ; :: thesis: verum