for M being non empty MetrSpace
for p being Point of M
for q being Point of (TopSpaceMetr M)
for r being Real st p = q & r > 0 holds
Ball (p,r) is a_neighborhood of q