let n be Nat; 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; 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); 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); ( 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)
; ( |.(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; verum