theorem :: TOPDIM_1:40

for TM being metrizable TopSpace
for Null, A being Subset of TM st TM | Null is second-countable & Null is finite-ind & A is finite-ind & ind Null <= 0 holds
( A \/ Null is finite-ind & ind (A \/ Null) <= (ind A) + 1 )