theorem :: TOPREAL6:61

for n being Nat
for w being Point of (Euclid n)
for A being Subset of (TOP-REAL n)
for r being Real st A = Sphere (w,r) holds
A is closed