:: deftheorem defines lim_filter FINTOPO8:def 1 :
for NTX being non empty strict U_FMT_filter FMT_Space_Str
for F being Filter of the carrier of NTX holds lim_filter F = { x where x is Point of NTX : F is_filter-finer_than U_FMT x } ;