let A, B, C, A1, B1, C2 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 & A,A1,C2 are_collinear & B,B1,C2 are_collinear holds
( (1 - mu) + (lambda * mu) <> 0 & ex alpha being Real st
( C2 = ((1 - alpha) * A) + (alpha * A1) & alpha = (1 - mu) / ((1 - mu) + (lambda * mu)) ) )
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 & A,A1,C2 are_collinear & B,B1,C2 are_collinear implies ( (1 - mu) + (lambda * mu) <> 0 & ex alpha being Real st
( C2 = ((1 - alpha) * A) + (alpha * A1) & alpha = (1 - mu) / ((1 - mu) + (lambda * mu)) ) ) )
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 and
A5: A,A1,C2 are_collinear and
A6: B,B1,C2 are_collinear ; :: thesis: ( (1 - mu) + (lambda * mu) <> 0 & ex alpha being Real st
( C2 = ((1 - alpha) * A) + (alpha * A1) & alpha = (1 - mu) / ((1 - mu) + (lambda * mu)) ) )
A7: A <> A1 by Th14, A1, A2;
A8: the_area_of_polygon3 (A,B,C) <> 0 by A1, Th9;
C2,A,A1 are_collinear by A5;
then C2 in Line (A,A1) by A7, Th13;
then consider alpha being Real such that
A9: C2 = ((1 - alpha) * A) + (alpha * A1) ;
0 = the_area_of_polygon3 (B,B1,C2) by A6, Th9
.= ((1 - mu) - (((1 - mu) + (lambda * mu)) * alpha)) * (the_area_of_polygon3 (A,B,C)) by Lm1, A9, A2, A3 ;
then A10: ( (1 - mu) - (((1 - mu) + (lambda * mu)) * alpha) = 0 & 1 - mu <> 0 ) by A8, A4;
then (1 - mu) + (lambda * mu) <> 0 ;
hence ( (1 - mu) + (lambda * mu) <> 0 & ex alpha being Real st
( C2 = ((1 - alpha) * A) + (alpha * A1) & alpha = (1 - mu) / ((1 - mu) + (lambda * mu)) ) ) by A9, A10, XCMPLX_1:89; :: thesis: verum