set T = the non empty strict discrete TopSpace;
reconsider NT = Top2NTop the non empty strict discrete TopSpace as NTopSpace ;
reconsider NT = NT as T_2 NTopSpace by Lm28;
A1: NTop2Top NT = the non empty strict discrete TopSpace by FINTOPO7:24;

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

let A, B be closed Subset of NT; :: thesis: ( A misses B implies ex V being a_neighborhood of A ex W being a_neighborhood of B st V misses W )
assume A2: A misses B ; :: thesis: ex V being a_neighborhood of A ex W being a_neighborhood of B st V misses W
reconsider TA = A, TB = B as closed Subset of the non empty strict discrete TopSpace by A1, Lm29;
consider G1, G2 being Subset of the non empty strict discrete TopSpace such that
A3: G1 is open and
A4: G2 is open and
A5: TA c= G1 and
A6: TB c= G2 and
A7: G1 misses G2 by A2, PRE_TOPC:def 12;
reconsider G1 = G1 as open Subset of the non empty strict discrete TopSpace by A3;
reconsider G2 = G2 as open Subset of the non empty strict discrete TopSpace by A4;
A8: ( TA c= Int G1 & TB c= Int G2 ) by A5, A6, TOPS_1:23;
reconsider V = G1, W = G2 as open Subset of NT by Lm1;
( Top2NTop G1 is a_neighborhood of Top2NTop TA & Top2NTop G2 is a_neighborhood of Top2NTop TB ) by A8, CONNSP_2:def 2, Lm31;
hence ex V being a_neighborhood of A ex W being a_neighborhood of B st V misses W by A7; :: thesis: verum

end;

then NT is normal ;
hence ex b₁ being NTopSpace st
( not b₁ is empty & b₁ is normal ) ; :: thesis: verum