theorem :: MSSUBFAM:47

for I being set
for A, B, M being ManySortedSet of I
for SF being MSSubsetFamily of M st A in SF & A c= B holds
meet SF c= B