let T be TopSpace; :: thesis: for n being Nat
for Af being finite-ind Subset of T holds
( ind Af <= n - 1 iff Af in (Seq_of_ind T) . n )
let n be Nat; :: thesis: for Af being finite-ind Subset of T holds
( ind Af <= n - 1 iff Af in (Seq_of_ind T) . n )
let Af be finite-ind Subset of T; :: thesis: ( ind Af <= n - 1 iff Af in (Seq_of_ind T) . n )
set I = ind Af;
A1: Af in (Seq_of_ind T) . ((ind Af) + 1) by Def5;
A2: (ind Af) + 1 is Nat by Lm3;

hereby :: thesis: ( Af in (Seq_of_ind T) . n implies ind Af <= n - 1 )

assume ind Af <= n - 1 ; :: thesis: Af in (Seq_of_ind T) . n
then A3: (ind Af) + 1 <= (n - 1) + 1 by XREAL_1:6;
( (ind Af) + 1 in NAT & n in NAT ) by A2, ORDINAL1:def 12;
then (Seq_of_ind T) . ((ind Af) + 1) c= (Seq_of_ind T) . n by A3, PROB_1:def 5;
hence Af in (Seq_of_ind T) . n by A1; :: thesis: verum

end;

assume A4: Af in (Seq_of_ind T) . n ; :: thesis: ind Af <= n - 1
assume ind Af > n - 1 ; :: thesis: contradiction
then A5: ind Af >= (n - 1) + 1 by INT_1:7;
then ( n in NAT & ind Af in NAT ) by INT_1:3;
then (Seq_of_ind T) . n c= (Seq_of_ind T) . (ind Af) by A5, PROB_1:def 5;
hence contradiction by A4, Def5; :: thesis: verum