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