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