let T be TopSpace; :: thesis: for Af being finite-ind Subset of T holds
( ind Af = - 1 iff Af is empty )
let Af be finite-ind Subset of T; :: thesis: ( ind Af = - 1 iff Af is empty )
not - 1 in dom (Seq_of_ind T) ;
then A1: not Af in (Seq_of_ind T) . (- 1) by FUNCT_1:def 2;
A2: (Seq_of_ind T) . 0 = {({} T)} by Def1;

hereby :: thesis: ( Af is empty implies ind Af = - 1 )

assume ind Af = - 1 ; :: thesis: Af is empty
then Af in (Seq_of_ind T) . ((- 1) + 1) by Def5;
hence Af is empty by A2, TARSKI:def 1; :: thesis: verum

end;

assume Af is empty ; :: thesis: ind Af = - 1
then A3: Af in (Seq_of_ind T) . 0 by A2, TARSKI:def 1;
(- 1) + 1 = 0 ;
hence ind Af = - 1 by A1, A3, Def5; :: thesis: verum