let n be Nat; :: thesis:
let Tf be finite-ind TopSpace; :: thesis:
set CT = [#] Tf;
set TT = Tf | ([#] Tf);
A1: [#] (Tf | ([#] Tf)) = [#] Tf by PRE_TOPC:def 10;
Tf is SubSpace of Tf by TSEP_1:2;
then A2: TopStruct(# the carrier of Tf,the topology of Tf #) = TopStruct(# the carrier of (Tf | ([#] Tf)),the topology of (Tf | ([#] Tf)) #) by A1, TSEP_1:5;
A3: [#] Tf is with_finite_small_inductive_dimension by Def4;

hereby :: thesis:

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

end;

assume A10: 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:

now

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

end;

hence ind Tf <= n by A3, Th9; :: thesis: