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 is_collinear & B,B1,C2 is_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 is_collinear & B,B1,C2 is_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
A: A,B,C is_a_triangle and
B: A1 = ((1 - lambda) * B) + (lambda * C) and
C: B1 = ((1 - mu) * C) + (mu * A) and
D: mu <> 1 and
E: A,A1,C2 is_collinear and
F: B,B1,C2 is_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)) ) )
H2: A <> A1 by Th14, A, B;
H3: the_area_of_polygon3 (A,B,C) <> 0 by A, Th9;
C2,A,A1 is_collinear by Th15, E;
then C2 in Line (A,A1) by H2, Th13;
then consider alpha being Real such that
G1: C2 = ((1 - alpha) * A) + (alpha * A1) ;
0 = the_area_of_polygon3 (B,B1,C2) by F, Th9
.= ((1 - mu) - (((1 - mu) + (lambda * mu)) * alpha)) * (the_area_of_polygon3 (A,B,C)) by Lm1, G1, B, C ;
then G3: ( (1 - mu) - (((1 - mu) + (lambda * mu)) * alpha) = 0 & 1 - mu <> 0 ) by H3, D;
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 G1, XCMPLX_1:89, G3; :: thesis: verum