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