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