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