:: deftheorem Def1 defines SingleMSS FACIRC_2:def 1 :
for x being set
for b₂ being void strict ManySortedSign holds
( b₂ = SingleMSS x iff the carrier of b₂ = {x} );