let T1, T2 be TopSpace; :: thesis: for A1 being Subset of T1
for A2 being Subset of T2 st A1,A2 are_homeomorphic holds
( A1 is with_finite_small_inductive_dimension iff A2 is with_finite_small_inductive_dimension )
let A1 be Subset of T1; :: thesis: for A2 being Subset of T2 st A1,A2 are_homeomorphic holds
( A1 is with_finite_small_inductive_dimension iff A2 is with_finite_small_inductive_dimension )
let A2 be Subset of T2; :: thesis: ( A1,A2 are_homeomorphic implies ( A1 is with_finite_small_inductive_dimension iff A2 is with_finite_small_inductive_dimension ) )
assume A1,A2 are_homeomorphic ; :: thesis: ( A1 is with_finite_small_inductive_dimension iff A2 is with_finite_small_inductive_dimension )
then A1: T1 | A1,T2 | A2 are_homeomorphic by METRIZTS:def 1;

hereby :: thesis: ( A2 is with_finite_small_inductive_dimension implies A1 is with_finite_small_inductive_dimension )

assume A1 is with_finite_small_inductive_dimension ; :: thesis: A2 is with_finite_small_inductive_dimension
then T2 | A2 is with_finite_small_inductive_dimension by A1, Lm9;
hence A2 is with_finite_small_inductive_dimension by Th18; :: thesis: verum

end;

assume A2 is with_finite_small_inductive_dimension ; :: thesis: A1 is with_finite_small_inductive_dimension
then T1 | A1 is with_finite_small_inductive_dimension by A1, Lm9;
hence A1 is with_finite_small_inductive_dimension by Th18; :: thesis: verum