for I being set
for M being ManySortedSet of I
for SF, SG being MSSubsetFamily of M holds SF (\+\) SG is MSSubsetFamily of M