theorem :: TOPDIM_2:23

for n being Nat
for TM being metrizable TopSpace st TM is second-countable & TM is finite-ind & ind TM <= n holds
for F being finite Subset-Family of TM st F is open & F is Cover of TM holds
ex G being finite Subset-Family of TM st
( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n )