:: deftheorem Def2 defines with_finite_small_inductive_dimension TOPDIM_1:def 2 :
for T being TopSpace
for A being Subset of T holds
( A is with_finite_small_inductive_dimension iff ex n being Nat st A in (Seq_of_ind T) . n );