let A, B, C be Point of (TOP-REAL 2); :: thesis: 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; :: thesis: ( 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).| ; :: thesis: A,B,C are_mutually_distinct
now :: thesis: ( not A = C & not B = C )
hereby :: thesis: not B = C
assume A = C ; :: thesis: contradiction
then r * |.(A - B).| = r * 0 by A4, EUCLID_6:42;
then |.(A - B).| = 0 by A2, XCMPLX_1:5;
hence contradiction by A1, EUCLID_6:42; :: thesis: verum
end;
hereby :: thesis: verum
assume B = C ; :: thesis: contradiction
then ( 1 * |.(A - B).| = r * |.(A - B).| & |.(A - B).| <> 0 ) by A1, A4, EUCLID_6:42;
hence contradiction by A3, XCMPLX_1:5; :: thesis: verum
end;
end;
hence A,B,C are_mutually_distinct by A1; :: thesis: verum