:: deftheorem Def4 defines with_finite_small_inductive_dimension TOPDIM_1:def 4 :
for T being TopSpace holds
( T is with_finite_small_inductive_dimension iff [#] T is with_finite_small_inductive_dimension );