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