theorem Th12: :: MESFUN16:12

for z being Point of RNS_Real
for x, r being Real st x = z holds
Ball (z,r) = ].(x - r),(x + r).[