let T be non empty TopSpace; :: thesis: ( T is regular & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite implies T is normal )
assume that
A1: T is regular and
A2: ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ; :: thesis: T is normal
consider Bn being FamilySequence of T such that
A3: Bn is Basis_sigma_locally_finite by A2;
A4: Union Bn is Basis of T by A3, Def6;
A5: Bn is sigma_locally_finite by A3, Def6;
for A being Subset of T
for U being open Subset of T st A is closed & U is open & A c= U holds
ex W being Function of NAT,(bool the carrier of T) st
( A c= Union W & Union W c= U & ( for n being Element of NAT holds
( Cl (W . n) c= U & W . n is open ) ) )

proof

let A be Subset of T; :: thesis: for U being open Subset of T st A is closed & U is open & A c= U holds
ex W being Function of NAT,(bool the carrier of T) st
( A c= Union W & Union W c= U & ( for n being Element of NAT holds
( Cl (W . n) c= U & W . n is open ) ) )
let U be open Subset of T; :: thesis: ( A is closed & U is open & A c= U implies ex W being Function of NAT,(bool the carrier of T) st
( A c= Union W & Union W c= U & ( for n being Element of NAT holds
( Cl (W . n) c= U & W . n is open ) ) ) )
assume that
A is closed and
U is open and
A6: A c= U ; :: thesis: ex W being Function of NAT,(bool the carrier of T) st
( A c= Union W & Union W c= U & ( for n being Element of NAT holds
( Cl (W . n) c= U & W . n is open ) ) )
deffunc H₁( set ) -> set = union { O where O is Subset of T : ( O in Bn . $1 & Cl O c= U ) } ;
A7: for k being set st k in NAT holds
H₁(k) in bool the carrier of T

proof

let k be set ; :: thesis: ( k in NAT implies H₁(k) in bool the carrier of T )
assume k in NAT ; :: thesis: H₁(k) in bool the carrier of T
then reconsider k = k as Element of NAT ;

now

let bu be set ; :: thesis: ( bu in H₁(k) implies bu in the carrier of T )
assume bu in H₁(k) ; :: thesis: bu in the carrier of T
then consider b being set such that
A8: bu in b and
A9: b in { O where O is Subset of T : ( O in Bn . k & Cl O c= U ) } by TARSKI:def 4;
ex O being Subset of T st
( b = O & O in Bn . k & Cl O c= U ) by A9;
hence bu in the carrier of T by A8; :: thesis: verum

end;

then H₁(k) c= the carrier of T by TARSKI:def 3;
hence H₁(k) in bool the carrier of T ; :: thesis: verum

end;

consider BU being Function of NAT,(bool the carrier of T) such that
A10: for k being set st k in NAT holds
BU . k = H₁(k) from FUNCT_2:sch 2(A7);

A11: now

let n be Element of NAT ; :: thesis: ( BU . n is open & Cl (BU . n) c= U )
set BUn = { O where O is Subset of T : ( O in Bn . n & Cl O c= U ) } ;
{ O where O is Subset of T : ( O in Bn . n & Cl O c= U ) } c= bool the carrier of T

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in { O where O is Subset of T : ( O in Bn . n & Cl O c= U ) } or b in bool the carrier of T )
assume b in { O where O is Subset of T : ( O in Bn . n & Cl O c= U ) } ; :: thesis: b in bool the carrier of T
then ex O being Subset of T st
( b = O & O in Bn . n & Cl O c= U ) ;
hence b in bool the carrier of T ; :: thesis: verum

end;

then reconsider BUn = { O where O is Subset of T : ( O in Bn . n & Cl O c= U ) } as Subset-Family of T ;
A12: BUn c= Bn . n

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in BUn or b in Bn . n )
assume b in BUn ; :: thesis: b in Bn . n
then ex O being Subset of T st
( b = O & O in Bn . n & Cl O c= U ) ;
hence b in Bn . n ; :: thesis: verum

end;

Bn . n is locally_finite by A5, Def3;
then A13: Cl (union BUn) = union (clf BUn) by A12, PCOMPS_1:12, PCOMPS_1:23;
A14: Cl (union BUn) c= U

proof

let ClBu be set ; :: according to TARSKI:def 3 :: thesis: ( not ClBu in Cl (union BUn) or ClBu in U )
assume ClBu in Cl (union BUn) ; :: thesis: ClBu in U
then consider ClB being set such that
A15: ClBu in ClB and
A16: ClB in clf BUn by A13, TARSKI:def 4;
reconsider ClB = ClB as Subset of T by A16;
consider B being Subset of T such that
A17: Cl B = ClB and
A18: B in BUn by A16, PCOMPS_1:def 3;
ex Q being Subset of T st
( B = Q & Q in Bn . n & Cl Q c= U ) by A18;
hence ClBu in U by A15, A17; :: thesis: verum

end;

BUn c= the topology of T

proof

let B be set ; :: according to TARSKI:def 3 :: thesis: ( not B in BUn or B in the topology of T )
assume B in BUn ; :: thesis: B in the topology of T
then consider Q being Subset of T such that
A19: B = Q and
A20: Q in Bn . n and
Cl Q c= U ;
A21: Union Bn c= the topology of T by A4, TOPS_2:78;
Q in Union Bn by A20, PROB_1:25;
hence B in the topology of T by A19, A21; :: thesis: verum

end;

then union BUn in the topology of T by PRE_TOPC:def 1;
then union BUn is open by PRE_TOPC:def 5;
hence ( BU . n is open & Cl (BU . n) c= U ) by A10, A14; :: thesis: verum

end;

A22: Union BU c= U

proof

let bu be set ; :: according to TARSKI:def 3 :: thesis: ( not bu in Union BU or bu in U )
assume bu in Union BU ; :: thesis: bu in U
then consider k being Element of NAT such that
A23: bu in BU . k by PROB_1:25;
bu in union { O where O is Subset of T : ( O in Bn . k & Cl O c= U ) } by A10, A23;
then consider b being set such that
A24: bu in b and
A25: b in { O where O is Subset of T : ( O in Bn . k & Cl O c= U ) } by TARSKI:def 4;
consider O being Subset of T such that
A26: b = O and
O in Bn . k and
A27: Cl O c= U by A25;
O c= Cl O by PRE_TOPC:48;
then b c= U by A26, A27, XBOOLE_1:1;
hence bu in U by A24; :: thesis: verum

end;

for a being set st a in A holds
a in Union BU

proof

let a be set ; :: thesis: ( a in A implies a in Union BU )
assume a in A ; :: thesis: a in Union BU
then consider Q being Subset of T such that
A28: a in Q and
A29: Cl Q c= U and
A30: Q in Union Bn by A1, A4, A6, Th19;
consider k being Element of NAT such that
A31: Q in Bn . k by A30, PROB_1:25;
Q in { O where O is Subset of T : ( O in Bn . k & Cl O c= U ) } by A29, A31;
then a in H₁(k) by A28, TARSKI:def 4;
then a in BU . k by A10;
hence a in Union BU by PROB_1:25; :: thesis: verum

end;

then A c= Union BU by TARSKI:def 3;
hence ex W being Function of NAT,(bool the carrier of T) st
( A c= Union W & Union W c= U & ( for n being Element of NAT holds
( Cl (W . n) c= U & W . n is open ) ) ) by A22, A11; :: thesis: verum

end;

hence T is normal by Th18; :: thesis: verum