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