theorem :: TOPREAL9:40

for n being Nat
for r being Real
for x being Point of (TOP-REAL n) st not n is zero & Sphere (x,r) is empty holds
r < 0 ;