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

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 )end;

hence
A,B,C are_mutually_distinct
by A1; :: thesis: verumhereby :: 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;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

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;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