let A, B, C, A1, B1 be Point of (TOP-REAL 2); :: thesis: for lambda, mu being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & mu <> 1 holds
( (1 - mu) + (lambda * mu) <> 0 iff not Line (A,A1) is_parallel_to Line (B,B1) )
let lambda, mu be Real; :: thesis: ( A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & mu <> 1 implies ( (1 - mu) + (lambda * mu) <> 0 iff not Line (A,A1) is_parallel_to Line (B,B1) ) )
assume that
A1: A,B,C is_a_triangle and
A2: A1 = ((1 - lambda) * B) + (lambda * C) and
A3: B1 = ((1 - mu) * C) + (mu * A) and
A4: mu <> 1 ; :: thesis: ( (1 - mu) + (lambda * mu) <> 0 iff not Line (A,A1) is_parallel_to Line (B,B1) )
A5: A <> A1 by A1, A2, Th14;
B,C,A is_a_triangle by A1;
then A6: B <> B1 by A3, Th14;

hereby :: thesis: ( not Line (A,A1) is_parallel_to Line (B,B1) implies (1 - mu) + (lambda * mu) <> 0 )

assume (1 - mu) + (lambda * mu) <> 0 ; :: thesis: not Line (A,A1) is_parallel_to Line (B,B1)
then consider C2 being Point of (TOP-REAL 2) such that
A7: ( A,A1,C2 are_collinear & B,B1,C2 are_collinear ) by Lm3, A1, A2, A3;
( C2,A,A1 are_collinear & C2,B,B1 are_collinear ) by A7;
then ( C2 in Line (A,A1) & C2 in Line (B,B1) ) by A5, A6, Th13;
hence not Line (A,A1) is_parallel_to Line (B,B1) by XBOOLE_0:3; :: thesis: verum

end;

assume not Line (A,A1) is_parallel_to Line (B,B1) ; :: thesis: (1 - mu) + (lambda * mu) <> 0
then consider C2 being object such that
A8: ( C2 in Line (A,A1) & C2 in Line (B,B1) ) by XBOOLE_0:3;
reconsider C2 = C2 as Point of (TOP-REAL 2) by A8;
( C2,A,A1 are_collinear & C2,B,B1 are_collinear ) by A8, A5, A6, Th13;
then ( A,A1,C2 are_collinear & B,B1,C2 are_collinear ) ;
hence (1 - mu) + (lambda * mu) <> 0 by Lm2, A1, A2, A3, A4; :: thesis: verum