theorem Th17: :: JORDAN2B:17

for u being Point of RealSpace
for r, u1 being Real st u1 = u holds
Ball (u,r) = { s where s is Real : ( u1 - r < s & s < u1 + r ) }