for T being TopSpace
for n being Nat holds
( ( T is finite-ind & ind T <= n ) iff ex Bas being Basis of T st
for A being Subset of T st A in Bas holds
( Fr A is finite-ind & ind (Fr A) <= n - 1 ) )