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