let E be non empty set ; :: thesis: for e being non empty Subset of E holds
( e is Singleton 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 Singleton of E iff for Y being set holds
( Y c= e iff ( Y = {} or Y = e ) ) )
thus ( e is Singleton 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 Singleton of E )

proof

assume A1: e is Singleton 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 object st e = {x} by A1, ZFMISC_1:131;
hence ( Y c= e iff ( Y = {} or Y = e ) ) by ZFMISC_1:33; :: thesis: verum

end;

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