theorem :: TOPREAL9:10

for n being Nat
for r being Real
for y being Point of (TOP-REAL n) st y in Ball ((0. (TOP-REAL n)),r) holds
|.y.| < r