theorem Th23: :: JORDAN:23
for n being Element of NAT
for x being Point of (TOP-REAL n)
for r being non zero Real holds Cl (Ball (x,r)) = cl_Ball (x,r)