theorem Th28: :: JORDAN1K:28

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