theorem :: MSSUBFAM:46

for I being set
for M being ManySortedSet of I
for SF, SG being MSSubsetFamily of M st SF c= SG holds
meet SG c= meet SF