:: deftheorem Def7 defines MSS-membered MSALIMIT:def 7 :
for X being set holds
( X is MSS-membered iff for x being set st x in X holds
x is non empty non void strict ManySortedSign );