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;
A1: { the Element of e} c= e ;
reconsider x = the Element of e as Element of E ;
{x} = e by A1, Th1;
hence ex a being Element of E st
( a in E & e = {a} ) ; :: thesis: verum