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

now :: thesis: for p, q being Point of T st p <> q holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & q in G2 & G1 misses G2 )

let p, q be Point of T; :: thesis: ( p <> q implies ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & q in G2 & G1 misses G2 ) )
assume A1: p <> q ; :: thesis: ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & q in G2 & G1 misses G2 )
reconsider p9 = p, q9 = q as Point of NT by FINTOPO7:def 16;
set Sp = lim_filter (U_FMT p9);
set Sq = lim_filter (U_FMT q9);
consider Vx being Element of U_FMT p9, Vy being Element of U_FMT q9 such that
A2: Vx misses Vy by A1, Th39;
p9 is_interior_point_of Vx by FINTOPO7:def 5;
then consider Ox being open Subset of NT such that
A3: p9 in Ox and
A4: Ox c= Vx by Lm4;
q9 is_interior_point_of Vy by FINTOPO7:def 5;
then consider Oy being open Subset of NT such that
A5: q9 in Oy and
A6: Oy c= Vy by Lm4;
reconsider G1 = Ox, G2 = Oy as open Subset of T by Lm9;
G1 misses G2 by A4, A6, A2, XBOOLE_1:64;
hence ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & q in G2 & G1 misses G2 ) by A3, A5; :: thesis: verum

end;

hence NTop2Top NT is non empty strict T_2 TopSpace by PRE_TOPC:def 10; :: thesis: verum