take TrivOrthoRelStr ; :: thesis: ( TrivOrthoRelStr is trivial & not TrivOrthoRelStr is empty & TrivOrthoRelStr is reflexive )
thus ( TrivOrthoRelStr is trivial & not TrivOrthoRelStr is empty & TrivOrthoRelStr is reflexive ) ; :: thesis: verum