:: deftheorem Def8 defines MSS_set MSALIMIT:def 9 :
for A being non empty set
for b₂ being set holds
( b₂ = MSS_set A iff for x being object holds
( x in b₂ iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) ) );