set X = {} ;
assume singletons {} <> {} ; :: thesis: contradiction
then consider f being set such that
A1: f in singletons {} by XBOOLE_0:def 1;
ex g being Subset of {} st
( g = f & g is Singleton ) by A1;
hence contradiction ; :: thesis: verum