theorem :: MSSUBFAM:44
for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M st EmptyMS I in SF holds
meet SF = EmptyMS I