theorem Th46: :: TOPREAL9:48
for a, b, r being Real
for x being Point of (Euclid 2) st x = |[a,b]| holds
Ball (x,r) = inside_of_circle (a,b,r)