theorem :: MSSUBFAM:49

for I being set
for M being ManySortedSet of I
for SF, SG, SH being MSSubsetFamily of M st SH = SF (\/) SG holds
meet SH = (meet SF) (/\) (meet SG)