let n be Nat; :: thesis: 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
let r be Real; :: thesis: for y being Point of (TOP-REAL n) st y in cl_Ball ((0. (TOP-REAL n)),r) holds
|.y.| <= r
let y be Point of (TOP-REAL n); :: thesis: ( y in cl_Ball ((0. (TOP-REAL n)),r) implies |.y.| <= r )
assume y in cl_Ball ((0. (TOP-REAL n)),r) ; :: thesis: |.y.| <= r
then |.(y - (0. (TOP-REAL n))).| <= r by Th6;
hence |.y.| <= r by RLVECT_1:13; :: thesis: verum