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