take TrivOrthoRelStr ; :: thesis: ( TrivOrthoRelStr is with_infima & TrivOrthoRelStr is with_suprema & TrivOrthoRelStr is strict )
thus ( TrivOrthoRelStr is with_infima & TrivOrthoRelStr is with_suprema & TrivOrthoRelStr is strict ) ; :: thesis: verum