take TrivialMSSign ; :: thesis: ( TrivialMSSign is strict & TrivialMSSign is empty & TrivialMSSign is void )
thus ( TrivialMSSign is strict & TrivialMSSign is empty & TrivialMSSign is void ) ; :: thesis: verum