( not [#] T is empty & [#] T is with_finite_small_inductive_dimension ) by Def4;
hence ind T is natural ; :: thesis: verum