let NT be normal NTopSpace; :: thesis:
reconsider T = NTop2Top NT as non empty TopSpace ;

let F1, F2 be Subset of T; :: thesis:
assume that
A1: F1 is closed and
A2: F2 is closed and
A3: F1 misses F2 ; :: thesis:
Top2NTop T = NT by FINTOPO7:25;
then reconsider F19 = F1, F29 = F2 as closed Subset of NT by A1, A2, Lm7;
consider V being a_neighborhood of F19, W being a_neighborhood of F29 such that
A4: V misses W by A3, Def13;
A5: ( NTop2Top F19 c= Int (NTop2Top V) & NTop2Top F29 c= Int (NTop2Top W) ) by Th36, CONNSP_2:def 2;
reconsider G1 = Int (NTop2Top V), G2 = Int (NTop2Top W) as open Subset of T ;
thus ex G1, G2 being Subset of T st
( G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2 ) by A4, A5, Th1; :: thesis:

end;