let T be non empty T_2 TopSpace; :: thesis: Top2NTop T is T_2 NTopSpace
reconsider NT = Top2NTop T as NTopSpace ;

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

let F be Filter of the carrier of NT; :: thesis: lim_filter F is trivial
set S = { x where x is Point of NT : 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 NT such that
A4: x = x9 and
A5: F is_filter-finer_than U_FMT x9 by A1;
consider y9 being Point of NT 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 T by FINTOPO7:def 15;
consider G1, G2 being Subset of T 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 A4, A6, A3, PRE_TOPC:def 10;
reconsider G19 = G1, G29 = G2 as open Subset of NT 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 G19 /\ G29 in F by A13, CARD_FIL:def 1;
hence contradiction by A12, CARD_FIL:def 1; :: thesis: verum

end;

hence lim_filter F is trivial ; :: thesis: verum

end;

then NT is T_2 ;
hence Top2NTop T is T_2 NTopSpace ; :: thesis: verum