let A, B, C, A1, B1, C1 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 holds
( A1,B1,C1 are_collinear iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = - 1 )
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 implies ( A1,B1,C1 are_collinear iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = - 1 ) )
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 & mu <> 1 & nu <> 1 ) ; :: thesis: ( A1,B1,C1 are_collinear iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = - 1 )
A6: the_area_of_polygon3 (A,B,C) <> 0 by Th9, A1;
set q = ((1 - lambda) * (1 - mu)) * (1 - nu);
A7: ( 1 - lambda <> 0 & 1 - mu <> 0 & 1 - nu <> 0 ) by A5;
( A1,B1,C1 are_collinear iff the_area_of_polygon3 (A1,B1,C1) = 0 ) by Th9;
then ( A1,B1,C1 are_collinear iff ((((1 - lambda) * (1 - mu)) * (1 - nu)) + ((lambda * mu) * nu)) * (the_area_of_polygon3 (A,B,C)) = 0 ) by Th17, A2, A3, A4;
then ( A1,B1,C1 are_collinear iff (1 * (((1 - lambda) * (1 - mu)) * (1 - nu))) + ((lambda * mu) * nu) = 0 ) by A6;
then ( A1,B1,C1 are_collinear iff (((1 - lambda) * (1 - mu)) * (1 - nu)) * (1 + (((lambda * mu) * nu) / (((1 - lambda) * (1 - mu)) * (1 - nu)))) = 0 ) by A7, XCMPLX_1:235;
then ( A1,B1,C1 are_collinear iff 1 + (((lambda * mu) * nu) / (((1 - lambda) * (1 - mu)) * (1 - nu))) = 0 ) by A7;
then ( A1,B1,C1 are_collinear iff - 1 = (lambda * (mu * nu)) / ((1 - lambda) * ((1 - mu) * (1 - nu))) ) ;
then ( A1,B1,C1 are_collinear iff - 1 = ((lambda / (1 - lambda)) * (mu * nu)) / ((1 - mu) * (1 - nu)) ) by XCMPLX_1:83;
then ( A1,B1,C1 are_collinear iff - 1 = (lambda / (1 - lambda)) * ((mu * nu) / ((1 - mu) * (1 - nu))) ) by XCMPLX_1:74;
then ( A1,B1,C1 are_collinear iff - 1 = (lambda / (1 - lambda)) * (((mu / (1 - mu)) * nu) / (1 - nu)) ) by XCMPLX_1:83;
then ( A1,B1,C1 are_collinear iff - 1 = (lambda / (1 - lambda)) * ((mu / (1 - mu)) * (nu / (1 - nu))) ) by XCMPLX_1:74;
hence ( A1,B1,C1 are_collinear iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = - 1 ) ; :: thesis: verum