:: deftheorem Def12 defines T_2 FINTOPO8:def 12 :
for NT being NTopSpace holds
( NT is T_2 iff for F being Filter of the carrier of NT holds lim_filter F is trivial );