let T be TopSpace; :: thesis: ( ex n being Nat st
for p being Point of T
for U being open Subset of T st p in U holds
ex W being open Subset of T st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) implies T is finite-ind )
given n being Nat such that A1: for p being Point of T
for U being open Subset of T st p in U holds
ex W being open Subset of T st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) ; :: thesis: T is finite-ind
set CT = [#] T;
set TT = T | ([#] T);
A2: [#] (T | ([#] T)) = [#] T by PRE_TOPC:def 5;
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 :: thesis: for p9 being Point of (T | ([#] T))
for U9 being open Subset of (T | ([#] T)) st p9 in U9 holds
ex W9 being open Subset of (T | ([#] T)) st
( p9 in W9 & W9 c= U9 & Fr W9 in (Seq_of_ind T) . n )

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

end;

then [#] T in (Seq_of_ind T) . (n + 1) by Def1;
then [#] T is finite-ind ;
hence T is finite-ind ; :: thesis: verum