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