theorem Th13: :: TOPDIM_2:13

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 for p being Point of TM
for U being open Subset of TM st p in U holds
ex W being open Subset of TM st
( p in W & W c= U & H /\ (Fr W) is finite-ind & ind (H /\ (Fr W)) <= n - 1 ) )