let n be Element of NAT ; :: thesis: for r being Real
for ep being Point of
for p, q being Point of 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
for p, q being Point of st p = ep & q in Ball ep,r holds
( |.(p - q).| < r & |.(q - p).| < r )
let ep be Point of ; :: thesis: for p, q being Point of st p = ep & q in Ball ep,r holds
( |.(p - q).| < r & |.(q - p).| < r )
let p, q be Point of ; :: 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 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