assume that
A2: M is finite-ind and
A3: ind M <= n ; :: 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: 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 U be open Subset of TM; :: thesis: ( p in U implies 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 ) )
assume A4: p in U ; :: thesis: 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 )
reconsider P = {p} as Subset of TM by A4, ZFMISC_1:31;
( not TM is empty & not p in U ` ) by A4, XBOOLE_0:def 5;
then consider L being Subset of TM such that
A5: L separates P,U ` and
A6: ind (L /\ M) <= n - 1 by A1, A2, A3, Th11, ZFMISC_1:50;
consider W, W1 being open Subset of TM 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: ( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )
( W c= W1 ` & W1 ` c= (U `) ` ) by A8, A9, SUBSET_1:12, SUBSET_1:23;
hence ( p in W & W c= U ) by A7, ZFMISC_1:31; :: thesis: ( M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )
Cl W misses W1 by A9, TSEP_1:36;
then (Cl W) \ W1 = Cl W by XBOOLE_1:83;
then Fr W = ((Cl W) \ W1) \ W by TOPS_1:42
.= (Cl W) \ (W \/ W1) by XBOOLE_1:41
.= (Cl W) /\ L by A10, SUBSET_1:13 ;
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 finite-ind by A2, TOPDIM_1:19;
then ind (M /\ (Fr W)) <= ind (M /\ L) by A11, TOPDIM_1:19;
hence ( M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) by A6, A11, A12, TOPDIM_1:19, XXREAL_0:2; :: thesis: verum

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