:: deftheorem defines with_finite_small_inductive_dimension TOPDIM_1:def 3 :
for T being TopSpace
for G being Subset-Family of T holds
( G is with_finite_small_inductive_dimension iff ex n being Nat st G c= (Seq_of_ind T) . n );