theorem Th16: :: TOPDIM_1:16

for n being Nat
for Tf being finite-ind TopSpace holds
( ind Tf <= n iff for p being Point of Tf
for U being open Subset of Tf st p in U holds
ex W being open Subset of Tf st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )