set T = 1TopSp X;
[#] (1TopSp X) in (Seq_of_ind (1TopSp X)) . 1 by Lm2;
then [#] (1TopSp X) is finite-ind ;
hence 1TopSp X is with_finite_small_inductive_dimension ; :: thesis: verum