let T be TopSpace; :: thesis: for n being Nat
for Af being finite-ind Subset of T holds
( ind Af <= n iff for p being Point of (T | Af)
for U being open Subset of (T | Af) st p in U holds
ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )
let n be Nat; :: thesis: for Af being finite-ind Subset of T holds
( ind Af <= n iff for p being Point of (T | Af)
for U being open Subset of (T | Af) st p in U holds
ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )
let Af be finite-ind Subset of T; :: thesis: ( ind Af <= n iff for p being Point of (T | Af)
for U being open Subset of (T | Af) st p in U holds
ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )
set I = ind Af;
A1: [#] (T | Af) c= [#] T by PRE_TOPC:def 4;
A2: ( Af in (Seq_of_ind T) . ((ind Af) + 1) & not Af in (Seq_of_ind T) . (ind Af) ) by Def5;

hereby :: thesis: ( ( for p being Point of (T | Af)
for U being open Subset of (T | Af) st p in U holds
ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) ) implies ind Af <= n )

assume A3: ind Af <= n ; :: thesis: for p being Point of (T | Af)
for U being open Subset of (T | Af) st p in U holds
ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
let p be Point of (T | Af); :: thesis: for U being open Subset of (T | Af) st p in U holds
ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
let U be open Subset of (T | Af); :: thesis: ( p in U implies ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )
assume A4: p in U ; :: thesis: ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
( not Af is empty & not T is empty ) by A4;
then reconsider I = ind Af as Nat by TARSKI:1;
A5: I - 1 <= n - 1 by A3, XREAL_1:9;
consider W being open Subset of (T | Af) such that
A6: ( p in W & W c= U ) and
A7: Fr W in (Seq_of_ind T) . I by A2, A4, Def1;
take W = W; :: thesis: ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
A8: Fr W in (Seq_of_ind (T | Af)) . I by A7, Th3;
then Fr W is finite-ind ;
then ind (Fr W) <= I - 1 by A8, Th7;
hence ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) by A5, A6, A8, XXREAL_0:2; :: thesis: verum

end;

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

now :: thesis: for p being Point of (T | Af)
for U being open Subset of (T | Af) st p in U holds
ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n )

let p be Point of (T | Af); :: thesis: for U being open Subset of (T | Af) st p in U holds
ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n )
let U be open Subset of (T | Af); :: thesis: ( p in U implies ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n ) )
assume p in U ; :: thesis: ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n )
then consider W being open Subset of (T | Af) such that
A10: ( p in W & W c= U ) and
A11: ( Fr W is finite-ind & ind (Fr W) <= n - 1 ) by A9;
A12: Fr W is Subset of T by A1, XBOOLE_1:1;
Fr W in (Seq_of_ind (T | Af)) . n by A11, Th7;
then Fr W in (Seq_of_ind T) . n by A12, Th3;
hence ex W being open Subset of (T | Af) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n ) by A10; :: thesis: verum

end;

then Af in (Seq_of_ind T) . (n + 1) by Def1;
then ind Af <= (n + 1) - 1 by Th7;
hence ind Af <= n ; :: thesis: verum