let T be TopSpace; :: thesis: for Af being finite-ind Subset of T holds (ind Af) + 1 is Nat
let Af be finite-ind Subset of T; :: thesis: (ind Af) + 1 is Nat
Af in (Seq_of_ind T) . (1 + (ind Af)) by Def5;
then (ind Af) + 1 in dom (Seq_of_ind T) by FUNCT_1:def 2;
hence (ind Af) + 1 is Nat ; :: thesis: verum