:: deftheorem Def1 defines meet MSSUBFAM:def 1 :
for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M
for b₄ being ManySortedSet of I holds
( b₄ = meet SF iff for i being object st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i & b₄ . i = Intersect Q ) );