let T be TopSpace; :: thesis:
let n be Nat; :: thesis:
set TOP = the topology of T;
set cT = the carrier of T;

hereby :: thesis:

defpred S₁[ set , set ] means for p being Point of T
for A being Subset of T st $1 = [p,A] holds
( $2 in the topology of T & ( not p in A implies $2 = {} T ) & ( p in A implies ex W being open Subset of T st
( W = $2 & p in W & W c= A & ind (Fr W) <= n - 1 ) ) );
assume that
A1: T is with_finite_small_inductive_dimension and
A2: ind T <= n ; :: thesis:
A3: for x being set st x in [:the carrier of T,the topology of T:] holds
ex y being set st S₁[x,y]

let x be set ; :: thesis:
assume x in [:the carrier of T,the topology of T:] ; :: thesis:
then consider p', A' being set such that
A4: p' in the carrier of T and
A5: A' in the topology of T and
A6: x = [p',A'] by ZFMISC_1:def 2;
reconsider p' = p' as Point of T by A4;
reconsider A' = A' as open Subset of T by A5, PRE_TOPC:def 5;

per cases ;

suppose A7: not p' in A' ; :: thesis:

take {} T ; :: thesis:
let p be Point of T; :: thesis:
let A be Subset of T; :: thesis:
assume A8: x = [p,A] ; :: thesis:
p = p' by A6, A8, ZFMISC_1:33;
hence ( {} T in the topology of T & ( not p in A implies {} T = {} T ) & ( p in A implies ex W being open Subset of T st
( W = {} T & p in W & W c= A & ind (Fr W) <= n - 1 ) ) ) by A6, A7, A8, PRE_TOPC:def 5, ZFMISC_1:33; :: thesis:

end;

suppose p' in A' ; :: thesis:

then consider W being open Subset of T such that
A9: ( p' in W & W c= A' ) and
Fr W is with_finite_small_inductive_dimension and
A10: ind (Fr W) <= n - 1 by A1, A2, Th16;
take W ; :: thesis:
let p be Point of T; :: thesis:
let A be Subset of T; :: thesis:
assume x = [p,A] ; :: thesis:
then ( p = p' & A = A' ) by A6, ZFMISC_1:33;
hence ( W in the topology of T & ( not p in A implies W = {} T ) & ( p in A implies ex W being open Subset of T st
( W = W & p in W & W c= A & ind (Fr W) <= n - 1 ) ) ) by A9, A10, PRE_TOPC:def 5; :: thesis:

end;

consider f being Function such that
A11: dom f = [:the carrier of T,the topology of T:] and
A12: for x being set st x in [:the carrier of T,the topology of T:] holds
S₁[x,f . x] from CLASSES1:sch 1(A3);
A13: rng f c= the topology of T

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
then consider x being set such that
A14: x in dom f and
A15: f . x = y by FUNCT_1:def 5;
ex p, A being set st
( p in the carrier of T & A in the topology of T & x = [p,A] ) by A11, A14, ZFMISC_1:def 2;
hence y in the topology of T by A11, A12, A14, A15; :: thesis:

end;

then reconsider RNG = rng f as Subset-Family of T by XBOOLE_1:1;

let A be Subset of T; :: thesis:
assume A is open ; :: thesis:
then A16: A in the topology of T by PRE_TOPC:def 5;
let p be Point of T; :: thesis:
assume A17: p in A ; :: thesis:
A18: [p,A] in [:the carrier of T,the topology of T:] by A16, A17, ZFMISC_1:106;
then consider W being open Subset of T such that
A19: ( W = f . [p,A] & p in W & W c= A ) and
ind (Fr W) <= n - 1 by A12, A17;
reconsider W = W as Subset of T ;
take W = W; :: thesis:
thus ( W in RNG & p in W & W c= A ) by A11, A18, A19, FUNCT_1:def 5; :: thesis:

end;

then reconsider RNG = RNG as Basis of T by A13, YELLOW_9:32;
take RNG = RNG; :: thesis:
let B be Subset of T; :: thesis:
assume B in RNG ; :: thesis:
then consider x being set such that
A20: x in dom f and
A21: f . x = B by FUNCT_1:def 5;
consider p, A being set such that
A22: p in the carrier of T and
A23: A in the topology of T and
A24: x = [p,A] by A11, A20, ZFMISC_1:def 2;

per cases ;

suppose p in A ; :: thesis:

then ex W being open Subset of T st
( W = f . [p,A] & p in W & W c= A & ind (Fr W) <= n - 1 ) by A11, A12, A20, A23, A24;
hence ( Fr B is with_finite_small_inductive_dimension & ind (Fr B) <= n - 1 ) by A1, A21, A24; :: thesis:

end;

suppose A25: not p in A ; :: thesis:

A26: not T is empty by A22;
B = {} T by A11, A12, A20, A21, A22, A23, A24, A25;
then A27: Fr B = {} T by A26, TOPGEN_1:41;
0 - 1 <= n - 1 by XREAL_1:11;
hence ( Fr B is with_finite_small_inductive_dimension & ind (Fr B) <= n - 1 ) by A27, Th6; :: thesis:

end;

given B being Basis of T such that A28: for A being Subset of T st A in B holds
( Fr A is with_finite_small_inductive_dimension & ind (Fr A) <= n - 1 ) ; :: thesis:

A29: now

let p be Point of T; :: thesis:
let U be open Subset of T; :: thesis:
assume p in U ; :: thesis:
then consider W being Subset of T such that
A30: W in B and
A31: ( p in W & W c= U ) by YELLOW_9:31;
B c= the topology of T by CANTOR_1:def 2;
then reconsider W = W as open Subset of T by A30, PRE_TOPC:def 5;
take W = W; :: thesis:
thus ( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= n - 1 ) by A28, A30, A31; :: thesis:

end;

then T is with_finite_small_inductive_dimension by Th15;
hence ( T is with_finite_small_inductive_dimension & ind T <= n ) by A29, Th16; :: thesis: