defpred S₁[ Nat] means for T1, T2 being TopSpace st T1,T2 are_homeomorphic & T1 is with_finite_small_inductive_dimension & ind T1 <= $1 holds
( T2 is with_finite_small_inductive_dimension & ind T2 <= ind T1 );
let T1, T2 be TopSpace; :: thesis:
assume that
A1: T1,T2 are_homeomorphic and
A2: T1 is with_finite_small_inductive_dimension ; :: thesis:
reconsider i = (ind T1) + 1 as Nat by A2, Lm3;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A4: S₁[n] ; :: thesis:
set n1 = n + 1;
let T1, T2 be TopSpace; :: thesis:
assume that
A5: T1,T2 are_homeomorphic and
A6: T1 is with_finite_small_inductive_dimension and
A7: ind T1 <= n + 1 ; :: thesis:
consider f being Function of T1,T2 such that
A8: f is being_homeomorphism by A5, T_0TOPSP:def 1;
set f9 = f " ;
A9: dom f = [#] T1 by A8, TOPS_2:def 5;
A10: rng f = [#] T2 by A8, TOPS_2:def 5;
B1: f is onto by A10, FUNCT_2:def 3;
A11: f is one-to-one by A8, TOPS_2:def 5;

per cases ;

suppose A12: [#] T1 = {} T1 ; :: thesis:

then ind T1 = - 1 by Th6;
hence ( T2 is with_finite_small_inductive_dimension & ind T2 <= ind T1 ) by A10, A12, Def4, Th6; :: thesis:

end;

suppose A13: [#] T1 <> {} T1 ; :: thesis:

then not T1 is empty ;
then reconsider i = ind T1 as Nat by A6;
A14: not T1 is empty by A13;
A15: not T2 is empty by A9, A13;

per cases by A7, NAT_1:8;

suppose i <= n ; :: thesis:

hence ( T2 is with_finite_small_inductive_dimension & ind T2 <= ind T1 ) by A4, A5, A6; :: thesis:

end;

suppose A16: ind T1 = n + 1 ; :: thesis:

A17: dom (f ") = [#] T2 by A10, A11, A15, TOPS_2:49;
A18: for p being Point of T2
for U being open Subset of T2 st p in U holds
ex W being open Subset of T2 st
( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= (n + 1) - 1 )

proof

reconsider F = f as Function ;
let p be Point of T2; :: thesis:
let U be open Subset of T2; :: thesis:
assume p in U ; :: thesis:
then A19: (f ") . p in (f ") .: U by A17, FUNCT_1:def 6;
( f " U = (f ") .: U & f " U is open ) by A8, A10, A11, A14, A15, TOPGRP_1:26, TOPS_2:55;
then consider W being open Subset of T1 such that
A20: (f ") . p in W and
A21: W c= f " U and
A22: Fr W is with_finite_small_inductive_dimension and
A23: ind (Fr W) <= (n + 1) - 1 by A6, A16, A19, Th16;
set FW = Fr W;
A24: ind (T1 | (Fr W)) = ind (Fr W) by A22, Lm5;
Fr W,f .: (Fr W) are_homeomorphic by A8, METRIZTS:3;
then A25: T1 | (Fr W),T2 | (f .: (Fr W)) are_homeomorphic by METRIZTS:def 1;
then T2 | (f .: (Fr W)) is with_finite_small_inductive_dimension by A4, A22, A23, A24;
then A26: f .: (Fr W) is with_finite_small_inductive_dimension by Th18;
F " = f " by B1, A11, TOPS_2:def 4;
then A27: f . ((f ") . p) = p by A10, A11, A15, FUNCT_1:35;
ind (T2 | (f .: (Fr W))) <= ind (T1 | (Fr W)) by A4, A22, A23, A24, A25;
then A28: ind (T2 | (f .: (Fr W))) <= (n + 1) - 1 by A23, A24, XXREAL_0:2;
reconsider W9 = f .: W as open Subset of T2 by A8, A14, A15, TOPGRP_1:25;
take W9 ; :: thesis:
W9 c= f .: (f " U) by A21, RELAT_1:123;
hence ( p in W9 & W9 c= U ) by A9, A10, A20, A27, FUNCT_1:77, FUNCT_1:def 6; :: thesis:
f .: (Fr W) = f .: ((Cl W) \ W) by TOPS_1:42
.= (f .: (Cl W)) \ W9 by A11, FUNCT_1:64
.= (Cl W9) \ W9 by A8, A15, TOPS_2:60
.= Fr W9 by TOPS_1:42 ;
hence ( Fr W9 is with_finite_small_inductive_dimension & ind (Fr W9) <= (n + 1) - 1 ) by A26, A28, Lm5; :: thesis:

end;

then T2 is with_finite_small_inductive_dimension by Th15;
hence ( T2 is with_finite_small_inductive_dimension & ind T2 <= ind T1 ) by A16, A18, Th16; :: thesis:

end;

A29: S₁[ 0 ]

proof

let T1, T2 be TopSpace; :: thesis:
assume that
A30: T1,T2 are_homeomorphic and
A31: T1 is with_finite_small_inductive_dimension and
A32: ind T1 <= 0 ; :: thesis:
consider f being Function of T1,T2 such that
A33: f is being_homeomorphism by A30, T_0TOPSP:def 1;
set f9 = f " ;
A34: dom f = [#] T1 by A33, TOPS_2:def 5;
A35: rng f = [#] T2 by A33, TOPS_2:def 5;
B1: f is onto by A35, FUNCT_2:def 3;
A36: f is one-to-one by A33, TOPS_2:def 5;

per cases ;

suppose A37: [#] T1 = {} T1 ; :: thesis:

then ind T1 = - 1 by Th6;
hence ( T2 is with_finite_small_inductive_dimension & ind T2 <= ind T1 ) by A35, A37, Def4, Th6; :: thesis:

end;

suppose A38: [#] T1 <> {} T1 ; :: thesis:

then not T1 is empty ;
then reconsider i = ind T1 as Nat by A31;
A39: i = 0 by A32;
A40: not T1 is empty by A38;
A41: not T2 is empty by A34, A38;
then A42: dom (f ") = [#] T2 by A35, A36, TOPS_2:49;
A43: for p being Point of T2
for U being open Subset of T2 st p in U holds
ex W being open Subset of T2 st
( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= 0 - 1 )

proof

reconsider F = f as Function ;
let p be Point of T2; :: thesis:
let U be open Subset of T2; :: thesis:
assume p in U ; :: thesis:
then A44: (f ") . p in (f ") .: U by A42, FUNCT_1:def 6;
F " = f " by B1, A36, TOPS_2:def 4;
then A45: f . ((f ") . p) = p by A35, A36, A41, FUNCT_1:35;
( f " U = (f ") .: U & f " U is open ) by A33, A35, A36, A40, A41, TOPGRP_1:26, TOPS_2:55;
then consider W being open Subset of T1 such that
A46: (f ") . p in W and
A47: W c= f " U and
A48: Fr W is with_finite_small_inductive_dimension and
A49: ind (Fr W) <= 0 - 1 by A31, A32, A44, Th16;
reconsider W9 = f .: W as open Subset of T2 by A33, A40, A41, TOPGRP_1:25;
take W9 ; :: thesis:
W9 c= f .: (f " U) by A47, RELAT_1:123;
hence ( p in W9 & W9 c= U ) by A34, A35, A45, A46, FUNCT_1:77, FUNCT_1:def 6; :: thesis:
ind (Fr W) >= - 1 by A48, Th5;
then ind (Fr W) = - 1 by A49, XXREAL_0:1;
then Fr W = {} T1 by A48, Th6;
then W is closed by TOPGEN_1:14;
then W9 is closed by A33, A41, TOPS_2:58;
then Fr W9 = {} T2 by TOPGEN_1:14;
hence ( Fr W9 is with_finite_small_inductive_dimension & ind (Fr W9) <= 0 - 1 ) by Th6; :: thesis:

end;

then T2 is with_finite_small_inductive_dimension by Th15;
hence ( T2 is with_finite_small_inductive_dimension & ind T2 <= ind T1 ) by A39, A43, Th16; :: thesis:

end;

A50: for n being Nat holds S₁[n] from NAT_1:sch 2(A29, A3);
(ind T1) + 0 <= i by XREAL_1:6;
hence ( T2 is with_finite_small_inductive_dimension & ind T2 <= ind T1 ) by A1, A2, A50; :: thesis: