for TM1, TM2 being second-countable finite-ind metrizable TopSpace st ( not TM1 is empty or not TM2 is empty ) holds
ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) by Lm5;