let A, B, C be 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
let r be Real; ( A <> B & r is positive & r <> 1 & |.(A - C).| = r * |.(A - B).| implies A,B,C are_mutually_distinct )
assume that
A1:
A <> B
and
A2:
r is positive
and
A3:
r <> 1
and
A4:
|.(A - C).| = r * |.(A - B).|
; A,B,C are_mutually_distinct
now ( not A = C & not B = C )end;
hence
A,B,C are_mutually_distinct
by A1; verum