:: deftheorem Def11 defines OneFS NUMBER17:def 11 :
for A being set
for b₂ being ManySortedSet of A holds
( b₂ = OneFS A iff for a being object st a in A holds
b₂ . a = <*a*> );