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 & (1 - mu) + (lambda * mu) <> 0 & (1 - lambda) + (nu * lambda) <> 0 & (1 - nu) + (mu * nu) <> 0 holds
( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff ex A2 being Point of (TOP-REAL 2) st
( A,A1,A2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_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 & (1 - mu) + (lambda * mu) <> 0 & (1 - lambda) + (nu * lambda) <> 0 & (1 - nu) + (mu * nu) <> 0 implies ( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff ex A2 being Point of (TOP-REAL 2) st
( A,A1,A2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear ) ) )
set q1 = (1 - mu) + (lambda * mu);
set q2 = (1 - lambda) + (nu * lambda);
set q3 = (1 - nu) + (mu * nu);
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: (1 - mu) + (lambda * mu) <> 0 and
A9: (1 - lambda) + (nu * lambda) <> 0 and
A10: (1 - nu) + (mu * nu) <> 0 ; :: thesis: ( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff ex A2 being Point of (TOP-REAL 2) st
( A,A1,A2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear ) )
B2: C,A,B is_a_triangle by Th15, A1;
B3: B,C,A is_a_triangle by Th15, A1;
consider C2 being Point of (TOP-REAL 2) such that
B4: A,A1,C2 is_collinear and
B5: B,B1,C2 is_collinear by Lm3, A1, A2, A3, A8;
consider B2 being Point of (TOP-REAL 2) such that
B6: C,C1,B2 is_collinear and
B7: A,A1,B2 is_collinear by Lm3, B2, A4, A2, A9;
consider A2 being Point of (TOP-REAL 2) such that
B8: B,B1,A2 is_collinear and
B9: C,C1,A2 is_collinear by Lm3, B3, A3, A4, A10;
D1: A <> A1 by Th14, A1, A2;
C2,A,A1 is_collinear by Th15, B4;
then D2: C2 in Line (A,A1) by D1, Th13;
B2,A,A1 is_collinear by Th15, B7;
then D3: B2 in Line (A,A1) by D1, Th13;

hereby :: thesis: ( ex A2 being Point of (TOP-REAL 2) st
( A,A1,A2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear ) implies ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 )

assume C1: ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 ; :: thesis: ex A2 being Point of (TOP-REAL 2) st
( A,A1,A2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear )

per cases ( B2 <> C2 or B2 = C2 ) ;

suppose C2: B2 <> C2 ; :: thesis: ex A2 being Point of (TOP-REAL 2) st
( A,A1,A2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear )

take A2 = A2; :: thesis: ( A,A1,A2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear )
A2,B2,C2 is_collinear by C1, Lm5, A1, A2, A3, A4, A5, A6, A7, B4, B5, B6, B7, B8, B9;
then C3: A2 in Line (B2,C2) by Th13, C2;
Line (B2,C2) c= Line (A,A1) by EUCLID_4:42, D2, D3;
then A2,A,A1 is_collinear by Th13, D1, C3;
hence A,A1,A2 is_collinear by Th15; :: thesis: ( B,B1,A2 is_collinear & C,C1,A2 is_collinear )
thus ( B,B1,A2 is_collinear & C,C1,A2 is_collinear ) by B8, B9; :: thesis: verum

end;

suppose C4: B2 = C2 ; :: thesis: ex B2 being Point of (TOP-REAL 2) st
( A,A1,B2 is_collinear & B,B1,B2 is_collinear & C,C1,B2 is_collinear )

take B2 = B2; :: thesis: ( A,A1,B2 is_collinear & B,B1,B2 is_collinear & C,C1,B2 is_collinear )
thus ( A,A1,B2 is_collinear & B,B1,B2 is_collinear & C,C1,B2 is_collinear ) by C4, B5, B6, B7; :: thesis: verum

end;

end;

end;

given C3 being Point of (TOP-REAL 2) such that C1: A,A1,C3 is_collinear and
C2: B,B1,C3 is_collinear and
C3: C,C1,C3 is_collinear ; :: thesis: ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1
C4: C3,B2,C2 is_collinear

proof

per cases ( B2 <> C2 or B2 = C2 ) ;

suppose C4: B2 <> C2 ; :: thesis: C3,B2,C2 is_collinear

C3,A,A1 is_collinear by Th15, C1;
then C5: C3 in Line (A,A1) by Th13, D1;
Line (A,A1) c= Line (B2,C2) by EUCLID_4:43, D2, D3, C4;
hence C3,B2,C2 is_collinear by C4, Th13, C5; :: thesis: verum

end;

suppose B2 = C2 ; :: thesis: C3,B2,C2 is_collinear

then not C3,B2,C2 are_mutually_different by ZFMISC_1:def 5;
hence C3,B2,C2 is_collinear by EUCLID_6:20; :: thesis: verum

end;

end;

end;

C3 = A2

proof

assume C5: C3 <> A2 ; :: thesis: contradiction
C,A,B is_a_triangle by Th15, A1;
then C7: C <> C1 by Th14, A4;
then C10: Line (C,C1) is being_line by EUCLID_4:def 4;
B,C,A is_a_triangle by Th15, A1;
then C8: B <> B1 by Th14, A3;
then C9: Line (B,B1) is being_line by EUCLID_4:def 4;
C3,B,B1 is_collinear by Th15, C2;
then H1: C3 in Line (B,B1) by Th13, C8;
A2,B,B1 is_collinear by Th15, B8;
then H2: A2 in Line (B,B1) by Th13, C8;
A2,C,C1 is_collinear by Th15, B9;
then H3: A2 in Line (C,C1) by Th13, C7;
C3,C,C1 is_collinear by Th15, C3;
then C3 in Line (C,C1) by Th13, C7;
then H4: Line (B,B1) = Line (C,C1) by EUCLID_4:44, H1, C5, H2, H3, C9, C10;
H5: 1 - nu <> 0 by A7;
B in Line (B,B1) by EUCLID_4:41;
then B,C,C1 is_collinear by Th13, C7, H4;
then the_area_of_polygon3 (B,C,C1) = 0 by Th9;
then the_area_of_polygon3 (C1,B,C) = 0 ;
then ((1 - nu) * (the_area_of_polygon3 (A,B,C))) + (nu * (the_area_of_polygon3 (B,B,C))) = 0 by Th7, A4;
then the_area_of_polygon3 (A,B,C) = 0 by H5;
hence contradiction by Th9, A1; :: thesis: verum

end;

hence ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 by C4, Lm5, A1, A2, A3, A4, A5, A6, A7, B4, B5, B6, B7, B8, B9; :: thesis: verum