let T be non empty TopSpace; :: thesis: ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite implies T is normal )
assume A1: ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ) ; :: thesis: T is normal
then consider Bn being FamilySequence of T such that
A2: Bn is Basis_sigma_locally_finite ;
A3: ( Union Bn is Basis of T & Bn is sigma_locally_finite ) by A2, 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 A4: ( A is closed & U is open & 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 ) } ;
A5: 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
A6: ( bu in b & 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
A7: ( b = O & O in Bn . k & Cl O c= U ) by A6;
thus bu in the carrier of T by A6, A7; :: 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
A8: for k being set st k in NAT holds
BU . k = H₁(k) from FUNCT_2:sch 2(A5);
A9: A c= Union BU

proof

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
A10: ( a in Q & Cl Q c= U & Q in Union Bn ) by A1, A3, A4, Th19;
consider k being Element of NAT such that
A11: Q in Bn . k by A10, PROB_1:25;
Q in { O where O is Subset of T : ( O in Bn . k & Cl O c= U ) } by A10, A11;
then a in H₁(k) by A10, TARSKI:def 4;
then a in BU . k by A8;
hence a in Union BU by PROB_1:25; :: thesis: verum

end;

hence A c= Union BU by TARSKI:def 3; :: thesis: verum

end;

A12: 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
A13: 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 A8, A13;
then consider b being set such that
A14: ( bu in b & 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
A15: ( b = O & O in Bn . k & Cl O c= U ) by A14;
O c= Cl O by PRE_TOPC:48;
then b c= U by A15, XBOOLE_1:1;
hence bu in U by A14; :: thesis: verum

end;

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 ) } ;
A16: Bn . n is locally_finite by A3, Def3;
{ 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 consider O being Subset of T such that
A17: ( b = O & O in Bn . n & Cl O c= U ) ;
thus b in bool the carrier of T by A17; :: 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 ;
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 consider O being Subset of T such that
A18: ( b = O & O in Bn . n & Cl O c= U ) ;
thus b in Bn . n by A18; :: thesis: verum

end;

then A19: Cl (union BUn) = union (clf BUn) by A16, PCOMPS_1:12, PCOMPS_1:23;
A20: 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
A21: ( ClBu in ClB & ClB in clf BUn ) by A19, TARSKI:def 4;
reconsider ClB = ClB as Subset of T by A21;
consider B being Subset of T such that
A22: ( Cl B = ClB & B in BUn ) by A21, PCOMPS_1:def 3;
consider Q being Subset of T such that
A23: ( B = Q & Q in Bn . n & Cl Q c= U ) by A22;
thus ClBu in U by A21, A22, A23; :: 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
A24: ( B = Q & Q in Bn . n & Cl Q c= U ) ;
( Q in Union Bn & Union Bn c= the topology of T ) by A3, A24, CANTOR_1:def 2, PROB_1:25;
hence B in the topology of T by A24; :: thesis: verum

end;

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

end;

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 A9, A12; :: thesis: verum

end;

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