for n being Element of NAT
for x being Point of (TOP-REAL n)
for r being non zero Real holds Fr (Ball (x,r)) = Sphere (x,r)