let E be non empty set ; :: thesis: ex e being Singleton of E st e is Singleton of E
take { the Element of E} ; :: thesis: { the Element of E} is Singleton of E
thus { the Element of E} is Singleton of E ; :: thesis: verum