let n be Element of 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:13;
dist ep,eq < r by A2, METRIC_1:12;
hence ( |.(p - q).| < r & |.(q - p).| < r ) by A1, JGRAPH_1:45; :: thesis: verum