let T be TopSpace; :: thesis: for Af being finite-ind Subset of T holds - 1 <= ind Af
let Af be finite-ind Subset of T; :: thesis: - 1 <= ind Af
Af in (Seq_of_ind T) . (1 + (ind Af)) by Def5;
then A1: (ind Af) + 1 in dom (Seq_of_ind T) by FUNCT_1:def 2;
0 = (- 1) + 1 ;
hence - 1 <= ind Af by A1, XREAL_1:6; :: thesis: verum