let A, B, C, A1 be Point of (TOP-REAL 2); :: thesis: for lambda being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) holds
A <> A1
let lambda be Real; :: thesis: ( A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) implies A <> A1 )
assume that
A: A,B,C is_a_triangle and
B: A1 = ((1 - lambda) * B) + (lambda * C) ; :: thesis: A <> A1
A,B,C are_mutually_different by A, EUCLID_6:20;
then H: ( A <> B & A <> C & B <> C ) by ZFMISC_1:def 5;

hereby :: thesis: verum

assume A = A1 ; :: thesis: contradiction
then A in Line (B,C) by B;
hence contradiction by H, Th13, A; :: thesis: verum

end;