let Tf be finite-ind TopSpace; :: thesis:
defpred S₁[ Nat] means for T being TopSpace st T is with_finite_small_inductive_dimension & ind T = $1 - 1 holds
for A being Subset of holds
( T | A is with_finite_small_inductive_dimension & ind (T | A) <= ind T );
[#] Tf is with_finite_small_inductive_dimension by Def4;
then reconsider i = (ind Tf) + 1 as Nat by Lm3;
A1: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

proof

let n' be Nat; :: thesis:
assume A2: for n being Nat st n < n' holds
S₁[n] ; :: thesis:

per cases ;

suppose A3: n' = 0 ; :: thesis:

let T be TopSpace; :: thesis:
assume that
A4: T is with_finite_small_inductive_dimension and
A5: ind T = n' - 1 ; :: thesis:
let A be Subset of ; :: thesis:
[#] T is with_finite_small_inductive_dimension by A4, Def4;
then [#] T = {} T by A3, A5, Th6;
hence ( T | A is with_finite_small_inductive_dimension & ind (T | A) <= ind T ) by A3, A5, Th6; :: thesis:

end;

suppose n' > 0 ; :: thesis:

then reconsider n = n' - 1 as Nat by NAT_1:20;
let T be TopSpace; :: thesis:
assume that
A6: T is with_finite_small_inductive_dimension and
A7: ind T = n' - 1 ; :: thesis:
let A be Subset of ; :: thesis:
set TA = T | A;
A8: [#] (T | A) = A by PRE_TOPC:def 10;

A9: now

let p be Point of ; :: thesis:
let U be open Subset of ; :: thesis:
assume A10: p in U ; :: thesis:
U in the topology of (T | A) by PRE_TOPC:def 5;
then consider U' being Subset of such that
A11: U' in the topology of T and
A12: U = U' /\ ([#] (T | A)) by PRE_TOPC:def 9;
A13: p in U' by A10, A12, XBOOLE_0:def 4;
then reconsider p' = p as Point of ;
U' is open Subset of by A11, PRE_TOPC:def 5;
then consider W' being open Subset of such that
A14: ( p' in W' & W' c= U' ) and
A15: Fr W' is with_finite_small_inductive_dimension and
A16: ind (Fr W') <= n - 1 by A6, A7, A13, Th16;
reconsider i = (ind (Fr W')) + 1 as Nat by A15, Lm3;
((ind (Fr W')) + 1) - 1 <= n - 1 by A16;
then ( n' - 1 < n' - 0 & (ind (Fr W')) + 1 <= n' - 1 ) by XREAL_1:11, XREAL_1:12;
then (ind (Fr W')) + 1 < n' by XXREAL_0:2;
then A17: S₁[i] by A2;
reconsider W = W' /\ ([#] (T | A)) as Subset of ;
W' in the topology of T by PRE_TOPC:def 5;
then W in the topology of (T | A) by PRE_TOPC:def 9;
then reconsider W = W as open Subset of by PRE_TOPC:def 5;
set FR' = Fr W';
set TF = T | (Fr W');
( [#] (T | (Fr W')) = Fr W' & Fr W c= (Fr W') /\ A ) by A8, Th1, PRE_TOPC:def 10;
then reconsider FrW = Fr W as Subset of by XBOOLE_1:18;
take W = W; :: thesis:
[#] (T | (Fr W')) c= [#] T by PRE_TOPC:def 9;
then reconsider FrW' = FrW as Subset of by XBOOLE_1:1;
A18: ( T | (Fr W') is with_finite_small_inductive_dimension & ind (T | (Fr W')) = ind (Fr W') ) by A15, Lm5;
then (T | (Fr W')) | FrW is with_finite_small_inductive_dimension by A17;
then A19: [#] ((T | (Fr W')) | FrW) is with_finite_small_inductive_dimension by Def4;
ind ((T | (Fr W')) | FrW) <= ind (Fr W') by A17, A18;
then ind ([#] ((T | (Fr W')) | FrW)) <= n - 1 by A16, XXREAL_0:2;
then ( [#] ((T | (Fr W')) | FrW) = FrW & [#] ((T | (Fr W')) | FrW) in (Seq_of_ind ((T | (Fr W')) | FrW)) . n ) by A19, Th7, PRE_TOPC:def 10;
then FrW in (Seq_of_ind (T | (Fr W'))) . n by Th3;
then FrW' in (Seq_of_ind T) . n by Th3;
then A20: Fr W in (Seq_of_ind (T | A)) . n by 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 A10, A12, A14, A20, Th7, XBOOLE_0:def 4, XBOOLE_1:26; :: thesis:

end;

then T | A is with_finite_small_inductive_dimension by Th15;
hence ( T | A is with_finite_small_inductive_dimension & ind (T | A) <= ind T ) by A7, A9, Th16; :: thesis:

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 4(A1);
then S₁[i] ;
hence for A being Subset of holds
( Tf | A is with_finite_small_inductive_dimension & ind (Tf | A) <= ind Tf ) ; :: thesis: