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 e is El_ev of E ; :: thesis: for Y being set holds
( Y c= e iff ( Y = {} or Y = e ) )
then consider x being set such that
A1: e = {x} by REALSET1:def 4;
let Y be set ; :: thesis: ( Y c= e iff ( Y = {} or Y = e ) )
thus ( Y c= e iff ( Y = {} or Y = e ) ) by A1, 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;
e is trivial

proof

{x} c= e by A3, ZFMISC_1:37;
then {x} = e by A2;
hence e is trivial by REALSET1:def 4; :: thesis: verum

end;

hence e is El_ev of E ; :: thesis: verum