theorem Th87: :: JORDAN2C:103

for n being 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 )