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

defpred S₁[ object , object ] 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 finite-ind and
A2: ind T <= n ; :: thesis:
A3: for x being object st x in [: the carrier of T, the topology of T:] holds
ex y being object st S₁[x,y]

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

take {} T ; :: thesis:
let p be Point of T; :: thesis:
let A be Subset of T; :: thesis:
assume A8: x = [p,A] ; :: thesis:
p = p9 by A6, A8, XTUPLE_0:1;
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 2, XTUPLE_0:1; :: thesis:

end;

then consider W being open Subset of T such that
A9: ( p9 in W & W c= A9 ) and
Fr W is finite-ind 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 = p9 & A = A9 ) by A6, XTUPLE_0:1;
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 2; :: thesis:

end;

consider f being Function such that
A11: dom f = [: the carrier of T, the topology of T:] and
A12: for x being object 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 object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
then consider x being object such that
A14: x in dom f and
A15: f . x = y by FUNCT_1:def 3;
ex p, A being object 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 2;
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:87;
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 3; :: 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 object such that
A20: x in dom f and
A21: f . x = B by FUNCT_1:def 3;
consider p, A being object 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;
reconsider A = A as set by TARSKI:1;

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 finite-ind & ind (Fr B) <= n - 1 ) by A1, A21, A24; :: thesis:

end;

end;

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

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 TOPS_2:64;
then reconsider W = W as open Subset of T by A30, PRE_TOPC:def 2;
take W = W; :: thesis:
thus ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) by A28, A30, A31; :: thesis:

end;