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
A1: A,B,C is_a_triangle and
A2: A1 = ((1 - lambda) * B) + (lambda * C) ; :: thesis: A <> A1
A,B,C are_mutually_distinct by A1, EUCLID_6:20;
then A3: ( 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 A2;
hence contradiction by A3, Th13, A1; :: thesis: verum

end;