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