for x, y being Real
for n being Nat
for e1, e2, e5, e6 being Point of (Euclid n)
for p1, p2 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e5 = y * p1 & e6 = y * p2 & dist (e1,e2) < x & y <> 0 holds
dist (e5,e6) < |.y.| * x