take TrivialUniformSpace ; :: thesis: ( TrivialUniformSpace is strict & TrivialUniformSpace is empty & not TrivialUniformSpace is void & TrivialUniformSpace is upper & TrivialUniformSpace is cap-closed & TrivialUniformSpace is axiom_U1 & TrivialUniformSpace is axiom_U2 & TrivialUniformSpace is axiom_U3 )
thus ( TrivialUniformSpace is strict & TrivialUniformSpace is empty & not TrivialUniformSpace is void & TrivialUniformSpace is upper & TrivialUniformSpace is cap-closed & TrivialUniformSpace is axiom_U1 & TrivialUniformSpace is axiom_U2 & TrivialUniformSpace is axiom_U3 ) ; :: thesis: verum