set U = the non empty set ;
take IT = { the Element of the non empty set * }; :: thesis: IT is trivial
thus IT is trivial ; :: thesis: verum