let T be non empty TopSpace; :: thesis:
assume A1: T is metrizable ; :: thesis:
then consider metr being Function of [:the carrier of T,the carrier of T:], REAL such that
A2: ( metr is_metric_of the carrier of T & Family_open_set (SpaceMetr the carrier of T,metr) = the topology of T ) by PCOMPS_1:def 9;
consider PM being non empty MetrStruct such that
A3: PM = SpaceMetr the carrier of T,metr ;
set TPM = TopSpaceMetr PM;
A4: [#] T = [#] (TopSpaceMetr PM) by A2, A3, PCOMPS_2:8;
deffunc H₁( Element of NAT ) -> set = { (Ball x,(1 / (2 |^ $1))) where x is Element of PM : x is Element of PM } ;
defpred S₁[ Element of NAT , set ] means $2 = H₁($1);
A5: for k being Element of NAT ex y being Subset-Family of T st S₁[k,y]

let k be Element of NAT ; :: thesis:
set Ak = H₁(k);
H₁(k) c= bool the carrier of T

let B be set ; :: according to TARSKI:def 3 :: thesis:
assume B in H₁(k) ; :: thesis:
then consider x being Element of PM such that
A6: ( B = Ball x,(1 / (2 |^ k)) & x is Element of PM ) ;
B in Family_open_set PM by A3, A6, PCOMPS_1:33;
hence B in bool the carrier of T by A2, A3; :: thesis:

end;

hence ex y being Subset-Family of T st S₁[k,y] ; :: thesis:

end;

consider FB being Function of NAT , bool (bool the carrier of T) such that
A7: for k being Element of NAT holds S₁[k,FB . k] from FUNCT_2:sch 3(A5);
A8: for n being Element of NAT ex PP being Subset-Family of T st
( PP is_finer_than FB . n & PP is Cover of T & PP is open & PP is locally_finite )

let n be Element of NAT ; :: thesis:
[#] (TopSpaceMetr PM) c= union (FB . n)

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in [#] (TopSpaceMetr PM) ; :: thesis:
then reconsider x' = x as Element of PM ;
( dist x',x' = 0 & 2 |^ n > 0 ) by A3, METRIC_1:1, NEWTON:102;
then dist x',x' < 1 / (2 |^ n) by XREAL_1:141;
then ( x' in Ball x',(1 / (2 |^ n)) & Ball x',(1 / (2 |^ n)) in H₁(n) ) by METRIC_1:12;
then ( x' in Ball x',(1 / (2 |^ n)) & Ball x',(1 / (2 |^ n)) in FB . n ) by A7;
hence x in union (FB . n) by TARSKI:def 4; :: thesis:

end;

then A13: FB . n is Cover of T by A4, SETFAM_1:def 12;
for U being Subset of T st U in FB . n holds
U is open

let U be Subset of T; :: thesis:
assume U in FB . n ; :: thesis:
then U in H₁(n) by A7;
then consider x being Element of PM such that
A14: ( U = Ball x,(1 / (2 |^ n)) & x is Element of PM ) ;
U in the topology of T by A2, A3, A14, PCOMPS_1:33;
hence U is open by PRE_TOPC:def 5; :: thesis:

end;

then FB . n is open by TOPS_2:def 1;
then ex PP being Subset-Family of T st
( PP is open & PP is Cover of T & PP is_finer_than FB . n & PP is locally_finite ) by A1, A13, PCOMPS_2:12;
hence ex PP being Subset-Family of T st
( PP is_finer_than FB . n & PP is Cover of T & PP is open & PP is locally_finite ) ; :: thesis:

end;

defpred S₂[ set , set ] means ex W being Subset-Family of T st
( W = $2 & W is open & W is Cover of T & W is_finer_than FB . $1 & W is locally_finite );
A15: for k being set st k in NAT holds
ex y being set st
( y in bool (bool the carrier of T) & S₂[k,y] )

let k be set ; :: thesis:
assume k in NAT ; :: thesis:
then reconsider k = k as Element of NAT ;
ex PP being Subset-Family of T st
( PP is_finer_than FB . k & PP is Cover of T & PP is open & PP is locally_finite ) by A8;
hence ex y being set st
( y in bool (bool the carrier of T) & S₂[k,y] ) ; :: thesis:

end;

consider UC being FamilySequence of T such that
A16: for x being set st x in NAT holds
S₂[x,UC . x] from FUNCT_2:sch 1(A15);
for n being Element of NAT holds UC . n is locally_finite

let n be Element of NAT ; :: thesis:
S₂[n,UC . n] by A16;
hence UC . n is locally_finite ; :: thesis:

end;

then A17: UC is sigma_locally_finite by Def3;
A18: Union UC c= the topology of T

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in Union UC ; :: thesis:
then consider k being Element of NAT such that
A19: u in UC . k by PROB_1:25;
reconsider u' = u as Subset of T by A19;
S₂[k,UC . k] by A16;
then u' is open by A19, TOPS_2:def 1;
hence u in the topology of T by PRE_TOPC:def 5; :: thesis:

end;

for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex B being Subset of T st
( B in Union UC & p in B & B c= A )

let A be Subset of T; :: thesis:
assume A20: A is open ; :: thesis:
let p be Point of T; :: thesis:
assume A21: p in A ; :: thesis:
A22: A in Family_open_set PM by A2, A3, A20, PRE_TOPC:def 5;
then reconsider p = p as Element of PM by A21;
consider r1 being Real such that
A23: ( r1 > 0 & Ball p,r1 c= A ) by A21, A22, PCOMPS_1:def 5;
consider n being Element of NAT such that
A24: 1 / (2 |^ n) <= r1 by A23, PREPOWER:106;
A25: S₂[n + 1,UC . (n + 1)] by A16;
then union (UC . (n + 1)) = the carrier of T by SETFAM_1:60;
then consider B being set such that
A26: ( p in B & B in UC . (n + 1) ) by TARSKI:def 4;
reconsider B = B as Subset of PM by A2, A3, A26, PCOMPS_2:8;
consider B1 being set such that
A27: ( B1 in FB . (n + 1) & B c= B1 ) by A25, A26, SETFAM_1:def 2;
B1 in H₁(n + 1) by A7, A27;
then consider q being Element of PM such that
A28: ( B1 = Ball q,(1 / (2 |^ (n + 1))) & q is Element of PM ) ;
A29: dist q,p < 1 / (2 |^ (n + 1)) by A26, A27, A28, METRIC_1:12;
B c= Ball p,r1

let r be Element of PM; :: thesis:
assume r in B ; :: thesis:
then A30: dist q,r < 1 / (2 |^ (n + 1)) by A27, A28, METRIC_1:12;
( dist p,q = dist q,p & dist q,r = dist r,q ) by A3, METRIC_1:3;
then A31: dist p,r <= (dist q,p) + (dist q,r) by A3, METRIC_1:4;
(dist q,p) + (dist q,r) < (1 / (2 |^ (n + 1))) + (1 / (2 |^ (n + 1))) by A29, A30, XREAL_1:10;
then dist p,r < 2 * (1 / (2 |^ (n + 1))) by A31, XXREAL_0:2;
then dist p,r < (1 / ((2 |^ n) * 2)) * 2 by NEWTON:11;
then dist p,r < 1 / (2 |^ n) by XCMPLX_1:93;
then dist p,r < r1 by A24, XXREAL_0:2;
hence r in Ball p,r1 by METRIC_1:12; :: thesis:

end;

hence B c= Ball p,r1 by SUBSET_1:7; :: thesis:

end;

then ( B in Union UC & p in B & B c= A ) by A23, A26, PROB_1:25, XBOOLE_1:1;
hence ex B being Subset of T st
( B in Union UC & p in B & B c= A ) ; :: thesis:

end;

then Union UC is Basis of T by A18, YELLOW_9:32;
then UC is Basis_sigma_locally_finite by A17, Def6;
hence ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite ; :: thesis: