theorem Th9: :: TOPDIM_1:9

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