for x being Point of FMT_R^1
for y being Point of RealSpace
for r being Real st x = y & r > 0 holds
Ball (y,r) is a_neighborhood of x