let x be set ; :: thesis: singletons {x} = {{x}}
A1: {x} c= {x} ;
thus singletons {x} c= {{x}} :: according to XBOOLE_0:def 10 :: thesis: {{x}} c= singletons {x}

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in singletons {x} or a in {{x}} )
assume a in singletons {x} ; :: thesis: a in {{x}}
then consider f being Subset of {x} such that
A2: a = f and
A3: f is 1 -element ;
( f = {} or f = {x} ) by ZFMISC_1:33;
hence a in {{x}} by A2, A3, TARSKI:def 1; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {{x}} or a in singletons {x} )
assume a in {{x}} ; :: thesis: a in singletons {x}
then a = {x} by TARSKI:def 1;
hence a in singletons {x} by A1; :: thesis: verum