:: deftheorem Def6 defines singleton SETWISEO:def 6 :
for A being set
for b₂ being Function of A,(Fin A) holds
( b₂ = singleton A iff for x being object st x in A holds
b₂ . x = {x} );