:: deftheorem defines Filter_Intersection CARDFIL2:def 4 :
for X, I being non empty set
for M being Filt b₁ -valued ManySortedSet of I holds Filter_Intersection M = meet (rng M);