theorem Th29: :: EUCLID12:37

for A, B, C being Point of (TOP-REAL 2)
for r being Real st A <> B & r is positive & r <> 1 & |.(A - C).| = r * |.(A - B).| holds
A,B,C are_mutually_distinct