set T2 = the non empty T_2 TopSpace;
reconsider NTX = Top2NTop the non empty T_2 TopSpace as NTopSpace ;
take NTX ; :: thesis: NTX is T_2

now :: thesis: for F being Filter of the carrier of NTX holds lim_filter F is trivial

let F be Filter of the carrier of NTX; :: thesis: lim_filter F is trivial
set S = { x where x is Point of NTX : F is_filter-finer_than U_FMT x } ;
for x, y being object holds
( not x in lim_filter F or not y in lim_filter F or not x <> y )

proof

let x, y be object ; :: thesis: ( not x in lim_filter F or not y in lim_filter F or not x <> y )
assume that
A1: x in lim_filter F and
A2: y in lim_filter F and
A3: x <> y ; :: thesis: contradiction
consider x9 being Point of NTX such that
A4: x = x9 and
A5: F is_filter-finer_than U_FMT x9 by A1;
consider y9 being Point of NTX such that
A6: y = y9 and
A7: F is_filter-finer_than U_FMT y9 by A2;
reconsider x99 = x9, y99 = y9 as Point of the non empty T_2 TopSpace by FINTOPO7:def 15;
consider G1, G2 being Subset of the non empty T_2 TopSpace such that
A8: G1 is open and
A9: G2 is open and
A10: x99 in G1 and
A11: y99 in G2 and
A12: G1 misses G2 by A3, A4, A6, PRE_TOPC:def 10;
reconsider G19 = G1, G29 = G2 as open Subset of NTX by A8, A9, Lm1;
A13: ( G19 in U_FMT x9 & G29 in U_FMT y9 ) by A10, A11, FINTOPO7:def 1;
( U_FMT x9 c= F & U_FMT y9 c= F ) by A5, A7, CARDFIL2:def 6;
then {} in F by A13, A12, CARD_FIL:def 1;
hence contradiction by CARD_FIL:def 1; :: thesis: verum

end;

hence lim_filter F is trivial ; :: thesis: verum

end;

hence NTX is T_2 ; :: thesis: verum