assume not singletons X is empty ; :: thesis: contradiction
then consider f being set such that
A1: f in singletons X by XBOOLE_0:def 1;
ex g being Subset of X st
( g = f & g is 1 -element ) by A1;
hence contradiction ; :: thesis: verum