let E be non empty set ; :: thesis: for e being El_ev of E holds card e = 1
let e be El_ev of E; :: thesis: card e = 1
ex a being Element of E st
( a in E & {a} = e ) by Th11;
hence card e = 1 by CARD_1:50; :: thesis: verum