theorem Th27: :: JORDAN1K:27

for p, q being Point of (TOP-REAL 2)
for r being Real st r <= 1 holds
dist (p,((r * p) + ((1 - r) * q))) = (1 - r) * (dist (p,q))