set s = the Element of S;
take { the Element of S} ; :: thesis: { the Element of S} is trivial
thus { the Element of S} is trivial ; :: thesis: verum