let T be TopSpace; :: thesis: ( T is empty implies T is with_finite_small_inductive_dimension )
assume T is empty ; :: thesis: T is with_finite_small_inductive_dimension
then [#] T is with_finite_small_inductive_dimension ;
hence T is with_finite_small_inductive_dimension by Def4; :: thesis: verum