take TrivOrthoRelStr ; :: thesis: ( TrivOrthoRelStr is OrderInvolutive & TrivOrthoRelStr is Pure & TrivOrthoRelStr is PartialOrdered )
thus ( TrivOrthoRelStr is OrderInvolutive & TrivOrthoRelStr is Pure & TrivOrthoRelStr is PartialOrdered ) ; :: thesis: verum