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