let X be non empty set ; :: thesis: ind (1TopSp X) = 0
set T = 1TopSp X;
(Seq_of_ind (1TopSp X)) . 0 = {({} (1TopSp X))} by Def1;
then A1: not [#] (1TopSp X) in (Seq_of_ind (1TopSp X)) . 0 by TARSKI:def 1;
A2: [#] (1TopSp X) in (Seq_of_ind (1TopSp X)) . (0 + 1) by Lm2;
then [#] (1TopSp X) is finite-ind ;
hence ind (1TopSp X) = 0 by A1, A2, Def5; :: thesis: verum