let E be non empty set ; :: thesis: for e being El_ev of E ex a being Element of E st
( a in E & e = {a} )
let e be El_ev of E; :: thesis: ex a being Element of E st
( a in E & e = {a} )
consider x being Element of e;
A1: {x} c= e ;
reconsider x = x as Element of E ;
( x in E & {x} = e ) by A1, Th1;
hence ex a being Element of E st
( a in E & e = {a} ) ; :: thesis: verum