let E be non empty set ; :: thesis: for a being Element of E holds {a} is El_ev of E
let a be Element of E; :: thesis: {a} is El_ev of E
set e = {a};
for Y being set holds
( {a} c= E & {a} <> {} & ( not Y c= {a} or Y = {} or Y = {a} ) & ( ( Y = {} or Y = {a} ) implies Y c= {a} ) ) by ZFMISC_1:39;
hence {a} is El_ev of E by Th1; :: thesis: verum