let n be Nat; :: thesis:
let TM be metrizable TopSpace; :: thesis:
set cTM = [#] TM;
set TOP = the topology of TM;
let M be Subset of TM; :: thesis:
assume A1: TM | M is second-countable ; :: thesis:

defpred S₁[ object , object ] means for p being Point of TM
for A being Subset of TM st $1 = [p,A] holds
( $2 in the topology of TM & ( not p in A implies $2 = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = $2 & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) );
assume A2: ( M is finite-ind & ind M <= n ) ; :: thesis:
A3: for x being object st x in [:([#] TM), the topology of TM:] holds
ex y being object st S₁[x,y]

let x be object ; :: thesis:
assume A4: x in [:([#] TM), the topology of TM:] ; :: thesis:
consider p9, A9 being object such that
A5: p9 in [#] TM and
A6: A9 in the topology of TM and
A7: x = [p9,A9] by A4, ZFMISC_1:def 2;
reconsider A9 = A9 as open Subset of TM by A6, PRE_TOPC:def 2;
reconsider p9 = p9 as Point of TM by A5;

take {} TM ; :: thesis:
let p be Point of TM; :: thesis:
let A be Subset of TM; :: thesis:
assume A9: x = [p,A] ; :: thesis:
p = p9 by A7, A9, XTUPLE_0:1;
hence ( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = {} TM & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) by A7, A8, A9, PRE_TOPC:def 2, XTUPLE_0:1; :: thesis:

end;

then consider W being open Subset of TM such that
A10: ( p9 in W & W c= A9 & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) by A1, A2, Th13;
take W ; :: thesis:
let p be Point of TM; :: thesis:
let A be Subset of TM; :: thesis:
assume A11: x = [p,A] ; :: thesis:
( p = p9 & A = A9 ) by A7, A11, XTUPLE_0:1;
hence ( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st
( W = W & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) by A10, PRE_TOPC:def 2; :: thesis:

end;

consider f being Function such that
A12: dom f = [:([#] TM), the topology of TM:] and
A13: for x being object st x in [:([#] TM), the topology of TM:] holds
S₁[x,f . x] from CLASSES1:sch 1(A3);
A14: rng f c= the topology of TM

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
then consider x being object such that
A15: x in dom f and
A16: f . x = y by FUNCT_1:def 3;
ex p, A being object st
( p in [#] TM & A in the topology of TM & x = [p,A] ) by A12, A15, ZFMISC_1:def 2;
hence y in the topology of TM by A12, A13, A15, A16; :: thesis:

end;

then reconsider RNG = rng f as Subset-Family of TM by XBOOLE_1:1;

let A be Subset of TM; :: thesis:
assume A17: A is open ; :: thesis:
A18: A in the topology of TM by A17, PRE_TOPC:def 2;
let p be Point of TM; :: thesis:
assume A19: p in A ; :: thesis:
A20: [p,A] in [:([#] TM), the topology of TM:] by A18, A19, ZFMISC_1:87;
then consider W being open Subset of TM such that
A21: ( W = f . [p,A] & p in W & W c= A ) and
M /\ (Fr W) is finite-ind and
ind (M /\ (Fr W)) <= n - 1 by A13, A19;
reconsider W = W as Subset of TM ;
take W = W; :: thesis:
thus ( W in RNG & p in W & W c= A ) by A12, A20, A21, FUNCT_1:def 3; :: thesis:

end;

then reconsider RNG = RNG as Basis of TM by A14, YELLOW_9:32;
take RNG = RNG; :: thesis:
let B be Subset of TM; :: thesis:
assume B in RNG ; :: thesis:
then consider x being object such that
A22: x in dom f and
A23: f . x = B by FUNCT_1:def 3;
consider p, A being object such that
A24: p in [#] TM and
A25: A in the topology of TM and
A26: x = [p,A] by A12, A22, ZFMISC_1:def 2;
reconsider A = A as open Subset of TM by A25, PRE_TOPC:def 2;

then ex W being open Subset of TM st
( W = f . [p,A] & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) by A12, A13, A22, A26;
hence ( M /\ (Fr B) is finite-ind & ind (M /\ (Fr B)) <= n - 1 ) by A23, A26; :: thesis:

end;

end;

given B being Basis of TM such that A28: for A being Subset of TM st A in B holds
( M /\ (Fr A) is finite-ind & ind (M /\ (Fr A)) <= n - 1 ) ; :: thesis:
for p being Point of TM
for U being open Subset of TM st p in U holds
ex W being open Subset of TM st
( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )

let p be Point of TM; :: thesis:
let U be open Subset of TM; :: thesis:
assume A29: p in U ; :: thesis:
consider a being Subset of TM such that
A30: a in B and
A31: ( p in a & a c= U ) by A29, YELLOW_9:31;
B c= the topology of TM by TOPS_2:64;
then reconsider a = a as open Subset of TM by A30, PRE_TOPC:def 2;
take a ; :: thesis:
thus ( p in a & a c= U & M /\ (Fr a) is finite-ind & ind (M /\ (Fr a)) <= n - 1 ) by A28, A30, A31; :: thesis:

end;