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 5;
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 finite-ind by Def4;

hereby :: thesis:

assume A4: ind Tf <= n ; :: thesis:
let p be Point of Tf; :: thesis:
let U be open Subset of Tf; :: thesis:
assume A5: p in U ; :: thesis:
reconsider p9 = p as Point of (Tf | ([#] Tf)) by A1;
U in the topology of Tf by PRE_TOPC:def 2;
then reconsider U9 = U as open Subset of (Tf | ([#] Tf)) by A2, PRE_TOPC:def 2;
consider W9 being open Subset of (Tf | ([#] Tf)) such that
A6: ( p9 in W9 & W9 c= U9 ) and
A7: ( Fr W9 is finite-ind & ind (Fr W9) <= n - 1 ) by A3, A4, A5, Th9;
W9 in the topology of (Tf | ([#] Tf)) by PRE_TOPC:def 2;
then reconsider W = W9 as open Subset of Tf by A2, PRE_TOPC:def 2;
not Tf is empty by A5;
then ( Cl W = Cl W9 & Int W = Int W9 ) by A1, TOPS_3:54;
then A8: Fr W = (Cl W9) \ (Int W9) by TOPGEN_1:8
.= Fr W9 by TOPGEN_1:8 ;
take W = W; :: thesis:
Fr W9 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 finite-ind ;
hence ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) by A6, A9, Th7; :: thesis:

end;

assume A10: for p being Point of Tf
for U being open Subset of Tf st p in U holds
ex W being open Subset of Tf st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) ; :: thesis:

now :: thesis:

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

end;

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