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

now :: thesis: for NA, NB being closed Subset of NT st NA misses NB holds
ex V being a_neighborhood of NA ex W being a_neighborhood of NB st V misses W

let NA, NB be closed Subset of NT; :: thesis: ( NA misses NB implies ex V being a_neighborhood of NA ex W being a_neighborhood of NB st V misses W )
assume A1: NA misses NB ; :: thesis: ex V being a_neighborhood of NA ex W being a_neighborhood of NB st V misses W
NTop2Top NT = T by FINTOPO7:24;
then reconsider A = NTop2Top NA, B = NTop2Top NB as closed Subset of T by Lm29;
consider G1, G2 being Subset of T such that
A2: G1 is open and
A3: G2 is open and
A4: A c= G1 and
A5: B c= G2 and
A6: G1 misses G2 by A1, PRE_TOPC:def 12;
reconsider V = Top2NTop G1, W = Top2NTop G2 as open Subset of NT by Lm1, A2, A3;
A7: ( A c= Int G1 & B c= Int G2 ) by A2, A3, A4, A5, TOPS_1:23;
reconsider V = G1, W = G2 as open Subset of NT by A2, A3, Lm1;
( Top2NTop G1 is a_neighborhood of Top2NTop A & Top2NTop G2 is a_neighborhood of Top2NTop B ) by A7, CONNSP_2:def 2, Lm31;
hence ex V being a_neighborhood of NA ex W being a_neighborhood of NB st V misses W by A6; :: thesis: verum

end;

hence Top2NTop T is normal ; :: thesis: verum