theorem Th58: :: FINTOPO8:58

for x being Point of FMT_R^1
for r being Real st r > 0 holds
].(x - r),(x + r).[ is a_neighborhood of x