let E be non empty set ; :: thesis: for e being non empty Subset of E holds
( e is El_ev of E iff for Y being set holds
( Y c= e iff ( Y = {} or Y = e ) ) )
let e be non empty Subset of E; :: thesis: ( e is El_ev of E iff for Y being set holds
( Y c= e iff ( Y = {} or Y = e ) ) )
thus ( e is El_ev of E implies for Y being set holds
( Y c= e iff ( Y = {} or Y = e ) ) ) :: thesis: ( ( for Y being set holds
( Y c= e iff ( Y = {} or Y = e ) ) ) implies e is El_ev of E )

proof

assume A1: e is El_ev of E ; :: thesis: for Y being set holds
( Y c= e iff ( Y = {} or Y = e ) )
let Y be set ; :: thesis: ( Y c= e iff ( Y = {} or Y = e ) )
ex x being set st e = {x} by A1, REALSET1:def 4;
hence ( Y c= e iff ( Y = {} or Y = e ) ) by ZFMISC_1:39; :: thesis: verum

end;

assume A2: for Y being set holds
( Y c= e iff ( Y = {} or Y = e ) ) ; :: thesis: e is El_ev of E
consider x being set such that
A3: x in e by XBOOLE_0:def 1;
{x} c= e by A3, ZFMISC_1:37;
then {x} = e by A2;
hence e is El_ev of E by REALSET1:def 4; :: thesis: verum