set X = {} ;
assume singletons {} <> {} ; :: thesis: contradiction
then consider f being set such that
A1: f in singletons {} by XBOOLE_0:def 1;
consider g being Subset of {} such that
g = f and
A2: g is Singleton by A1;
consider x being set such that
A3: x in {} and
g = {x} by A2;
thus contradiction by A3; :: thesis: verum