for n being Nat
for TM being metrizable TopSpace
for H being Subset of TM st TM | H is second-countable holds
( ( H is finite-ind & ind H <= n ) iff ex Bas being Basis of TM st
for A being Subset of TM st A in Bas holds
( H /\ (Fr A) is finite-ind & ind (H /\ (Fr A)) <= n - 1 ) )