theorem Th48: :: TOPREAL9:50
for a, b, r being Real holds Ball (|[a,b]|,r) = inside_of_circle (a,b,r)