for T being TopSpace
for G being Subset-Family of T
for I being Integer holds
( G is finite-ind & ind G <= I iff ( - 1 <= I & ( for A being Subset of T st A in G holds
( A is finite-ind & ind A <= I ) ) ) )