take the non empty trivial Subset of X ; :: thesis: the non empty trivial Subset of X is 1 -element
thus the non empty trivial Subset of X is 1 -element ; :: thesis: verum