take M = DiscreteSpace {{}}; :: thesis: ( M is trivial & not M is empty )
thus ( M is trivial & not M is empty ) ; :: thesis: verum