let T be TopSpace; :: thesis:
let G be Subset-Family of T; :: thesis:
let I be Integer; :: thesis:

hereby :: thesis:

assume that
A1: G is finite-ind and
A2: ind G <= I ; :: thesis:
ind G >= - 1 by A1, Def6;
then (ind G) + 1 >= (- 1) + 1 by XREAL_1:6;
then (ind G) + 1 in NAT by INT_1:3;
then reconsider iG = (ind G) + 1 as Nat ;
A3: G c= (Seq_of_ind T) . iG by A1, Def6;
- 1 <= ind G by A1, Def6;
hence - 1 <= I by A2, XXREAL_0:2; :: thesis:
let A be Subset of T; :: thesis:
assume A4: A in G ; :: thesis:
thus A is finite-ind by A1, A4; :: thesis:
then ind A <= iG - 1 by A3, A4, Th7;
hence ind A <= I by A2, XXREAL_0:2; :: thesis:

end;

assume that
A5: - 1 <= I and
A6: for A being Subset of T st A in G holds
( A is finite-ind & ind A <= I ) ; :: thesis:
(- 1) + 1 <= I + 1 by A5, XREAL_1:6;
then reconsider I1 = I + 1 as Element of NAT by INT_1:3;
A7: G c= (Seq_of_ind T) . I1

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A8: x in G ; :: thesis:
reconsider A = x as Subset of T by A8;
A9: I = I1 - 1 ;
( A is finite-ind & ind A <= I ) by A6, A8;
hence x in (Seq_of_ind T) . I1 by A9, Th7; :: thesis:

end;

then G is finite-ind ;
hence ( G is finite-ind & ind G <= I ) by A5, A7, Def6; :: thesis: