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