:: deftheorem defines lim_filterb CARDFIL2:def 25 :
for T being non empty TopSpace
for F being Filter of (BoolePoset ([#] T)) holds lim_filterb F = { x where x is Point of T : NeighborhoodSystem x c= F } ;