theorem :: MSSUBFAM:48

for I being set
for A, B, M being ManySortedSet of I
for SF being MSSubsetFamily of M st A in SF & A (/\) B = EmptyMS I holds
(meet SF) (/\) B = EmptyMS I