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 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 Wlet A,
B be
closed Subset of
NT;
( 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
;
ex V being a_neighborhood of A ex W being a_neighborhood of B st V misses Wreconsider 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;
verum end;
then
NT is normal
;
hence
ex b1 being NTopSpace st
( not b1 is empty & b1 is normal )
; verum