theorem Th13: :: TOPREAL9:15

for n being Nat
for r being Real
for x being Point of (TOP-REAL n)
for e being Point of (Euclid n) st x = e holds
Sphere (e,r) = Sphere (x,r)