theorem :: FINTOPO8:60

for x being Point of FMT_R^1
for y being Point of RealSpace
for r being Real st x = y holds
Ball (y,r) = ].(x - r),(x + r).[ by FRECHET:7;