for n being Nat
for M being non empty TopSpace
for q being Point of M
for r being real number
for p being Point of (TOP-REAL n) st r > 0 holds
for U being a_neighborhood of q st M | U, Tball (p,r) are_homeomorphic holds
ex W being a_neighborhood of q st
( W c= Int U & M | W, Tdisk (p,r) are_homeomorphic )