theorem :: TOPREAL9:11

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