let A be Subset of TM; :: thesis: ( A is countable implies A is with_finite_small_inductive_dimension )
assume A1: A is countable ; :: thesis: A is with_finite_small_inductive_dimension
TM | A is T_4 ;
hence A is with_finite_small_inductive_dimension by A1, Th19; :: thesis: verum