theorem Th26: :: JORDAN1K:26

for p, q being Point of (TOP-REAL 2)
for r being Real holds dist ((r * p),(r * q)) = |.r.| * (dist (p,q))