let n be Element of NAT ; :: thesis: for r being real number
for y being Point of (TOP-REAL n) st y in Ball (0.REAL n),r holds
|.y.| < r
let r be real number ; :: thesis: for y being Point of (TOP-REAL n) st y in Ball (0.REAL n),r holds
|.y.| < r
let y be Point of (TOP-REAL n); :: thesis: ( y in Ball (0.REAL n),r implies |.y.| < r )
assume y in Ball (0.REAL n),r ; :: thesis: |.y.| < r
then |.(y - (0.REAL n)).| < r by Th7;
hence |.y.| < r by JORDAN2C:13; :: thesis: verum