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