take TrivOrthoRelStr ; :: thesis: ( TrivOrthoRelStr is 1 -element & TrivOrthoRelStr is reflexive )
thus ( TrivOrthoRelStr is 1 -element & TrivOrthoRelStr is reflexive ) ; :: thesis: verum