theorem :: TOPDIM_2:24

for n being Nat
for TM being metrizable TopSpace st TM is finite-ind holds
for A being Subset of TM st ind (A `) <= n & TM | (A `) is second-countable holds
for A1, A2 being closed Subset of TM st A = A1 \/ A2 holds
ex X1, X2 being closed Subset of TM st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 )