theorem Th45: :: TOPREAL9:47
for a, b, r being Real
for x being Point of (Euclid 2) st x = |[a,b]| holds
cl_Ball (x,r) = closed_inside_of_circle (a,b,r)