let T be TopSpace; :: thesis: for A being Subset of T st T | A is with_finite_small_inductive_dimension holds
A is with_finite_small_inductive_dimension
let A be Subset of T; :: thesis: ( T | A is with_finite_small_inductive_dimension implies A is with_finite_small_inductive_dimension )
assume T | A is with_finite_small_inductive_dimension ; :: thesis: A is with_finite_small_inductive_dimension
then consider n being Nat such that
A1: [#] (T | A) in (Seq_of_ind (T | A)) . n by Def2;
[#] (T | A) = A by PRE_TOPC:def 5;
then A in (Seq_of_ind T) . n by A1, Th3;
hence A is with_finite_small_inductive_dimension by Def2; :: thesis: verum