let A, B, C, A1, B1, C1, A2, B2, C2 be Point of (TOP-REAL 2); :: thesis: for lambda, mu, nu being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C1 = ((1 - nu) * A) + (nu * B) & lambda <> 1 & mu <> 1 & nu <> 1 & A,A1,B2,C2 are_collinear & B,B1,A2,C2 are_collinear & C,C1,A2,B2 are_collinear holds
( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff A2,B2,C2 are_collinear )
let lambda, mu, nu be Real; :: thesis: ( A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C1 = ((1 - nu) * A) + (nu * B) & lambda <> 1 & mu <> 1 & nu <> 1 & A,A1,B2,C2 are_collinear & B,B1,A2,C2 are_collinear & C,C1,A2,B2 are_collinear implies ( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff A2,B2,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: C1 = ((1 - nu) * A) + (nu * B) and
A5: lambda <> 1 and
A6: mu <> 1 and
A7: nu <> 1 and
A8: A,A1,B2,C2 are_collinear and
A9: B,B1,A2,C2 are_collinear and
A10: C,C1,A2,B2 are_collinear ; :: thesis: ( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff A2,B2,C2 are_collinear )
set q = ((1 - lambda) * (1 - mu)) * (1 - nu);
A11: ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 ) by Lm4, A5, A6, A7;
A12: ( (((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu)) <> 0 & the_area_of_polygon3 (A2,B2,C2) = (((((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda))) ^2) / ((((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu)))) * (the_area_of_polygon3 (A,B,C)) ) by Th19, A1, A2, A3, A4, A5, A6, A7, A8, A9, A10;
the_area_of_polygon3 (A,B,C) <> 0 by Th9, A1;
hence ( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff A2,B2,C2 are_collinear ) by A12, Th9, A11; :: thesis: verum