assume
not singletons X is empty
; :: thesis: contradiction

then consider f being object such that

A1: f in singletons X ;

ex g being Subset of X st

( g = f & g is 1 -element ) by A1;

hence contradiction ; :: thesis: verum

then consider f being object such that

A1: f in singletons X ;

ex g being Subset of X st

( g = f & g is 1 -element ) by A1;

hence contradiction ; :: thesis: verum