let n be Nat; :: thesis:
let TM be metrizable TopSpace; :: thesis:
let M be Subset of ; :: thesis:
assume A1: TM | M is second-countable ; :: thesis:

hereby :: thesis:

assume that
A2: M is with_finite_small_inductive_dimension and
A3: ind M <= n ; :: thesis:
let p be Point of ; :: thesis:
let U be open Subset of ; :: thesis:
assume A4: p in U ; :: thesis:
reconsider P = {p} as Subset of by A4, ZFMISC_1:37;
( not TM is empty & not p in U ` ) by A4, XBOOLE_0:def 5;
then consider L being Subset of such that
A5: L separates P,U ` and
A6: ind (L /\ M) <= n - 1 by A1, A2, A3, Th11, ZFMISC_1:56;
consider W, W1 being open Subset of such that
A7: P c= W and
A8: U ` c= W1 and
A9: W misses W1 and
A10: L = (W \/ W1) ` by A5, METRIZTS:def 3;
take W = W; :: thesis:
( W c= W1 ` & W1 ` c= (U ` ) ` ) by A8, A9, SUBSET_1:31, SUBSET_1:43;
hence ( p in W & W c= U ) by A7, XBOOLE_1:1, ZFMISC_1:37; :: thesis:
Cl W misses W1 by A9, TSEP_1:40;
then (Cl W) \ W1 = Cl W by XBOOLE_1:83;
then Fr W = ((Cl W) \ W1) \ W by TOPS_1:76
.= (Cl W) \ (W \/ W1) by XBOOLE_1:41
.= (Cl W) /\ L by A10, SUBSET_1:32 ;
then Fr W c= L by XBOOLE_1:17;
then A11: M /\ (Fr W) c= M /\ L by XBOOLE_1:27;
M /\ L c= M by XBOOLE_1:17;
then A12: M /\ L is with_finite_small_inductive_dimension by A2, TOPDIM_1:19;
then ind (M /\ (Fr W)) <= ind (M /\ L) by A11, TOPDIM_1:19;
hence ( M /\ (Fr W) is with_finite_small_inductive_dimension & ind (M /\ (Fr W)) <= n - 1 ) by A6, A11, A12, TOPDIM_1:19, XXREAL_0:2; :: thesis:

end;

set Tm = TM | M;
assume A13: for p being Point of
for U being open Subset of st p in U holds
ex W being open Subset of st
( p in W & W c= U & M /\ (Fr W) is with_finite_small_inductive_dimension & ind (M /\ (Fr W)) <= n - 1 ) ; :: thesis:
A14: for p being Point of
for U being open Subset of st p in U holds
ex W being open Subset of st
( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= n - 1 )

proof

A15: [#] (TM | M) = M by PRE_TOPC:def 10;
let p be Point of ; :: thesis:
let U be open Subset of ; :: thesis:
assume A16: p in U ; :: thesis:
p in M by A15, A16;
then reconsider p' = p as Point of ;
consider U' being Subset of such that
A17: U' is open and
A18: U = U' /\ the carrier of (TM | M) by TSP_1:def 1;
p' in U' by A16, A18, XBOOLE_0:def 4;
then consider W' being open Subset of such that
A19: ( p' in W' & W' c= U' ) and
A20: M /\ (Fr W') is with_finite_small_inductive_dimension and
A21: ind (M /\ (Fr W')) <= n - 1 by A13, A17;
reconsider W = W' /\ the carrier of (TM | M) as Subset of by XBOOLE_1:17;
reconsider W = W as open Subset of by TSP_1:def 1;
take W ; :: thesis:
thus ( p in W & W c= U ) by A16, A18, A19, XBOOLE_0:def 4, XBOOLE_1:26; :: thesis:
reconsider FrW = Fr W as Subset of by A15, XBOOLE_1:1;
A22: FrW c= (Fr W') /\ M by A15, TOPDIM_1:1;
then A23: FrW is with_finite_small_inductive_dimension by A20, TOPDIM_1:19;
ind FrW <= ind ((Fr W') /\ M) by A20, A22, TOPDIM_1:19;
then ind (Fr W) <= ind ((Fr W') /\ M) by A23, TOPDIM_1:21;
hence ( Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= n - 1 ) by A21, A23, TOPDIM_1:21, XXREAL_0:2; :: thesis:

end;

then A24: TM | M is with_finite_small_inductive_dimension by TOPDIM_1:15;
then A25: M is with_finite_small_inductive_dimension by TOPDIM_1:18;
ind (TM | M) <= n by A14, A24, TOPDIM_1:16;
hence ( M is with_finite_small_inductive_dimension & ind M <= n ) by A25, TOPDIM_1:17; :: thesis: