theorem :: CLOSURE3:2

for I being set
for M, N being ManySortedSet of I
for F being SubsetFamily of M st N in F holds
meet |:F:| c=' N by CLOSURE2:21, MSSUBFAM:43;