:: deftheorem defines singletons BSPACE:def 8 :
for X being set holds singletons X = { f where f is Subset of X : f is 1 -element } ;