theorem :: CLOSURE2:6

for I being set
for M being ManySortedSet of I
for SF, SG being SubsetFamily of M holds SF \+\ SG is SubsetFamily of M ;