let T be non empty TopSpace; :: thesis:
assume that
A1: T is regular and
A2: ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ; :: thesis:
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 ) ) )

let A be Subset of T; :: thesis:
let U be open Subset of T; :: thesis:
assume that
A is closed and
U is open and
A6: A c= U ; :: thesis:
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

let k be object ; :: thesis:
assume k in NAT ; :: thesis:
then reconsider k = k as Element of NAT ;

let bu be object ; :: thesis:
assume bu in H₁(k) ; :: thesis:
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:

end;

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);

let n be Element of NAT ; :: thesis:
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

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in { O where O is Subset of T : ( O in Bn . n & Cl O c= U ) } ; :: thesis:
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:

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

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

end;

let ClBu be object ; :: according to TARSKI:def 3 :: thesis:
assume ClBu in Cl (union BUn) ; :: thesis:
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:

end;

let B be object ; :: according to TARSKI:def 3 :: thesis:
assume B in BUn ; :: thesis:
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:

end;

end;

let bu be object ; :: according to TARSKI:def 3 :: thesis:
assume bu in Union BU ; :: thesis:
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:

end;

let a be object ; :: thesis:
assume a in A ; :: thesis:
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:

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:

end;