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) & (1 - mu) + (lambda * mu) <> 0 holds
ex C2 being Point of (TOP-REAL 2) st
( A,A1,C2 is_collinear & B,B1,C2 is_collinear )
let lambda, mu be Real; :: thesis: ( A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & (1 - mu) + (lambda * mu) <> 0 implies ex C2 being Point of (TOP-REAL 2) st
( A,A1,C2 is_collinear & B,B1,C2 is_collinear ) )
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: (1 - mu) + (lambda * mu) <> 0 ; :: thesis: ex C2 being Point of (TOP-REAL 2) st
( A,A1,C2 is_collinear & B,B1,C2 is_collinear )
B2: A <> A1 by Th14, A1, A2;
consider alpha being Real such that
B3: alpha = (1 - mu) / ((1 - mu) + (lambda * mu)) ;
consider C2 being Point of (TOP-REAL 2) such that
B4: C2 = ((1 - alpha) * A) + (alpha * A1) ;
take C2 ; :: thesis: ( A,A1,C2 is_collinear & B,B1,C2 is_collinear )
C2 in Line (A,A1) by B4;
then C2,A,A1 is_collinear by B2, Th13;
hence A,A1,C2 is_collinear by Th15; :: thesis: B,B1,C2 is_collinear
the_area_of_polygon3 (B,B1,C2) = ((1 - mu) - (((1 - mu) / ((1 - mu) + (lambda * mu))) * ((1 - mu) + (lambda * mu)))) * (the_area_of_polygon3 (A,B,C)) by B3, Lm1, A2, A3, B4
.= ((1 - mu) - (1 - mu)) * (the_area_of_polygon3 (A,B,C)) by XCMPLX_1:87, A4 ;
hence B,B1,C2 is_collinear by Th9; :: thesis: verum