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