let E be non empty set ; :: thesis: for e being Singleton of E ex a being Element of E st
( a in E & e = {a} )
let e be Singleton of E; :: thesis: ex a being Element of E st
( a in E & e = {a} )
set x = the Element of e;
{ the Element of e} = e by Th1;
hence ex a being Element of E st
( a in E & e = {a} ) ; :: thesis: verum