let T be TopSpace; :: thesis:
given n being Nat such that A1: 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 ) ; :: thesis:
set CT = [#] T;
set TT = T | ([#] T);
A2: [#] (T | ([#] T)) = [#] T by PRE_TOPC:def 10;
T is SubSpace of T by TSEP_1:2;
then A3: TopStruct(# the carrier of T,the topology of T #) = TopStruct(# the carrier of (T | ([#] T)),the topology of (T | ([#] T)) #) by A2, TSEP_1:5;

now

let p' be Point of ; :: thesis:
let U' be open Subset of ; :: thesis:
assume A4: p' in U' ; :: thesis:
reconsider p = p' as Point of by A2;
U' in the topology of (T | ([#] T)) by PRE_TOPC:def 5;
then reconsider U = U' as open Subset of by A3, PRE_TOPC:def 5;
consider W being open Subset of such that
A5: p in W and
A6: ( W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= n - 1 ) by A1, A4;
W in the topology of T by PRE_TOPC:def 5;
then reconsider W' = W as open Subset of by A3, PRE_TOPC:def 5;
take W' = W'; :: thesis:
not T is empty by A5;
then ( Cl W = Cl W' & Int W = Int W' ) by A2, TOPS_3:54;
then Fr W = (Cl W') \ (Int W') by TOPGEN_1:10
.= Fr W' by TOPGEN_1:10 ;
hence ( p' in W' & W' c= U' & Fr W' in (Seq_of_ind T) . n ) by A5, A6, Th7; :: thesis:

end;

then [#] T in (Seq_of_ind T) . (n + 1) by Def1;
then [#] T is with_finite_small_inductive_dimension by Def2;
hence T is with_finite_small_inductive_dimension by Def4; :: thesis: