theorem Th61: :: FINTOPO8:61

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