let I be set ; :: thesis: for M being ManySortedSet of I
for SF, SG being MSSubsetFamily of M holds SF (\+\) SG is MSSubsetFamily of M
let M be ManySortedSet of I; :: thesis: for SF, SG being MSSubsetFamily of M holds SF (\+\) SG is MSSubsetFamily of M
let SF, SG be MSSubsetFamily of M; :: thesis: SF (\+\) SG is MSSubsetFamily of M
( SF (\) SG is MSSubsetFamily of M & SG (\) SF is MSSubsetFamily of M ) by Th36;
hence SF (\+\) SG is MSSubsetFamily of M by Th34; :: thesis: verum