theorem :: CARDFIL2:9

for X, I being non empty set
for M being Filt b₁ -valued ManySortedSet of I
for i being Element of I
for F being Filter of X st F = M . i holds
Filter_Intersection M is_filter-coarser_than F