let n be Element of NAT ; :: thesis: for p being Point of (Euclid n)
for x, p9 being Point of (TOP-REAL n)
for r being real number st p = p9 & |.(x - p9).| < r holds
x in Ball p,r
let p be Point of (Euclid n); :: thesis: for x, p9 being Point of (TOP-REAL n)
for r being real number st p = p9 & |.(x - p9).| < r holds
x in Ball p,r
let x, p9 be Point of (TOP-REAL n); :: thesis: for r being real number st p = p9 & |.(x - p9).| < r holds
x in Ball p,r
let r be real number ; :: thesis: ( p = p9 & |.(x - p9).| < r implies x in Ball p,r )
reconsider x9 = x as Point of (Euclid n) by TOPREAL3:13;
assume ( p = p9 & |.(x - p9).| < r ) ; :: thesis: x in Ball p,r
then dist x9,p < r by SPPOL_1:62;
hence x in Ball p,r by METRIC_1:12; :: thesis: verum