let T be TopSpace; :: thesis: for Af being finite-ind Subset of T holds
( T | Af is finite-ind & ind (T | Af) = ind Af )
let Af be finite-ind Subset of T; :: thesis: ( T | Af is finite-ind & ind (T | Af) = ind Af )
set TA = T | Af;
A1: [#] (T | Af) = Af by PRE_TOPC:def 5;

per cases ( ind Af = - 1 or not Af is empty ) by Th6;

suppose A2: ind Af = - 1 ; :: thesis: ( T | Af is finite-ind & ind (T | Af) = ind Af )

then Af = {} T by Th6;
hence ( T | Af is finite-ind & ind (T | Af) = ind Af ) by A2, Th6; :: thesis: verum

end;

suppose A3: not Af is empty ; :: thesis: ( T | Af is finite-ind & ind (T | Af) = ind Af )

then not T is empty ;
then reconsider n = ind Af as Nat by A3, TARSKI:1;
Af in (Seq_of_ind T) . (n + 1) by Def5;
then A4: [#] (T | Af) in (Seq_of_ind (T | Af)) . (n + 1) by A1, Th3;
then A5: [#] (T | Af) is finite-ind ;
hence T | Af is finite-ind ; :: thesis: ind (T | Af) = ind Af
A6: ind ([#] (T | Af)) >= n

proof

assume ind ([#] (T | Af)) < n ; :: thesis: contradiction
then (ind ([#] (T | Af))) + 1 <= n by INT_1:7;
then ((ind ([#] (T | Af))) + 1) - 1 <= n - 1 by XREAL_1:9;
then [#] (T | Af) in (Seq_of_ind (T | Af)) . n by A5, Th7;
then Af in (Seq_of_ind T) . n by A1, Th3;
hence contradiction by Def5; :: thesis: verum

end;

ind ([#] (T | Af)) <= (n + 1) - 1 by A4, A5, Th7;
hence ind (T | Af) = ind Af by A6, XXREAL_0:1; :: thesis: verum

end;

end;