let n be Nat; :: thesis: for p being Point of (Euclid n)
for x, p9 being Point of (TOP-REAL n)
for r being Real st p = p9 & x in Ball (p,r) holds
|.(x - p9).| < r
let p be Point of (Euclid n); :: thesis: for x, p9 being Point of (TOP-REAL n)
for r being Real st p = p9 & x in Ball (p,r) holds
|.(x - p9).| < r
let x, p9 be Point of (TOP-REAL n); :: thesis: for r being Real st p = p9 & x in Ball (p,r) holds
|.(x - p9).| < r
let r be Real; :: thesis: ( p = p9 & x in Ball (p,r) implies |.(x - p9).| < r )
reconsider x9 = x as Point of (Euclid n) by TOPREAL3:8;
assume that
A1: p = p9 and
A2: x in Ball (p,r) ; :: thesis: |.(x - p9).| < r
dist (x9,p) < r by A2, METRIC_1:11;
hence |.(x - p9).| < r by A1, SPPOL_1:39; :: thesis: verum