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;
A5: Bn is sigma_locally_finite by A3;
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 sequence of (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 sequence of (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 sequence of (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 sequence of (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₁( object ) -> set = union { O where O is Subset of T : ( O in Bn . $1 & Cl O c= U ) } ;
A7: for k being object st k in NAT holds
H₁(k) in bool the carrier of T

proof

let k be object ; :: 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 :: thesis: for bu being object st bu in H₁(k) holds
bu in the carrier of T

let bu be object ; :: 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 ;
hence H₁(k) in bool the carrier of T ; :: thesis: verum

end;

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

A11: now :: thesis: for n being Element of NAT holds
( BU . n is open & Cl (BU . n) c= U )

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 object ; :: 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 object ; :: 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;
then A13: Cl (union BUn) = union (clf BUn) by A12, PCOMPS_1:9, PCOMPS_1:20;
A14: Cl (union BUn) c= U

proof

let ClBu be object ; :: 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 2;
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 object ; :: 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:64;
Q in Union Bn by A20, PROB_1:12;
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 2;
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 object ; :: 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 Nat such that
A23: bu in BU . k by PROB_1:12;
A24: k in NAT by ORDINAL1:def 12;
bu in union { O where O is Subset of T : ( O in Bn . k & Cl O c= U ) } by A10, A23, A24;
then consider b being set such that
A25: bu in b and
A26: 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
A27: b = O and
O in Bn . k and
A28: Cl O c= U by A26;
O c= Cl O by PRE_TOPC:18;
then b c= U by A27, A28;
hence bu in U by A25; :: thesis: verum

end;

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

proof

let a be object ; :: 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
A29: a in Q and
A30: Cl Q c= U and
A31: Q in Union Bn by A1, A4, A6, Th19;
consider k being Nat such that
A32: Q in Bn . k by A31, PROB_1:12;
A33: k in NAT by ORDINAL1:def 12;
Q in { O where O is Subset of T : ( O in Bn . k & Cl O c= U ) } by A30, A32;
then a in H₁(k) by A29, TARSKI:def 4;
then a in BU . k by A10, A33;
hence a in Union BU by PROB_1:12; :: thesis: verum

end;

then A c= Union BU ;
hence ex W being sequence of (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