:: deftheorem defines lim_filter CARDFIL2:def 22 :
for T being non empty TopSpace
for F being Filter of the carrier of T holds lim_filter F = { x where x is Point of T : F is_filter-finer_than NeighborhoodSystem x } ;