let X be non empty set ; :: thesis: for f being Subset of X st f is Element of singletons X holds
f is 1 -element
let f be Subset of X; :: thesis: ( f is Element of singletons X implies f is 1 -element )
assume f is Element of singletons X ; :: thesis: f is 1 -element
then f in singletons X ;
then ex g being Subset of X st
( g = f & g is 1 -element ) ;
hence f is 1 -element ; :: thesis: verum