theorem Th17: :: TOPDIM_2:17

for u being Point of (Euclid 1)
for r, u1 being Real st <*u1*> = u holds
cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }