take the Element of X ; :: thesis: the Element of X is X -set
thus the Element of X is X -set ; :: thesis: verum