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