theorem Th7: :: TOPDIM_1:7

for T being TopSpace
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 )