let E be non empty set ; :: thesis: ex e being El_ev of E st e is El_ev of E
set a = the Element of E;
{ the Element of E} is El_ev of E by Th7;
hence ex e being El_ev of E st e is El_ev of E ; :: thesis: verum