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 are_collinear & B,B1,A2 are_collinear & C,C1,A2 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 & (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 are_collinear & B,B1,A2 are_collinear & C,C1,A2 are_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 are_collinear & B,B1,A2 are_collinear & C,C1,A2 are_collinear ) )
A11: C,A,B is_a_triangle by A1;
A12: B,C,A is_a_triangle by A1;
consider C2 being Point of (TOP-REAL 2) such that
A13: A,A1,C2 are_collinear and
A14: B,B1,C2 are_collinear by Lm3, A1, A2, A3, A8;
consider B2 being Point of (TOP-REAL 2) such that
A15: C,C1,B2 are_collinear and
A16: A,A1,B2 are_collinear by Lm3, A11, A4, A2, A9;
consider A2 being Point of (TOP-REAL 2) such that
A17: B,B1,A2 are_collinear and
A18: C,C1,A2 are_collinear by Lm3, A12, A3, A4, A10;
A19: A <> A1 by Th14, A1, A2;
C2,A,A1 are_collinear by A13;
then A20: C2 in Line (A,A1) by A19, Th13;
B2,A,A1 are_collinear by A16;
then A21: B2 in Line (A,A1) by A19, Th13;
A22: A,A1,B2,C2 are_collinear by A13, A16, A19, RLTOPSP1:81;
B,C,A is_a_triangle by A1;
then B <> B1 by Th14, A3;
then A23: B,B1,A2,C2 are_collinear by A14, A17, RLTOPSP1:81;
C,A,B is_a_triangle by A1;
then C <> C1 by Th14, A4;
then A24: C,C1,A2,B2 are_collinear by A15, A18, RLTOPSP1:81;

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

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

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

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

take A2 = A2; :: thesis: ( A,A1,A2 are_collinear & B,B1,A2 are_collinear & C,C1,A2 are_collinear )
A2,B2,C2 are_collinear by A25, Lm7, A1, A2, A3, A4, A5, A6, A7, A22, A23, A24;
then A27: A2 in Line (B2,C2) by Th13, A26;
Line (B2,C2) c= Line (A,A1) by A20, A21, EUCLID_4:42;
then A2,A,A1 are_collinear by Th13, A19, A27;
hence A,A1,A2 are_collinear ; :: thesis: ( B,B1,A2 are_collinear & C,C1,A2 are_collinear )
thus ( B,B1,A2 are_collinear & C,C1,A2 are_collinear ) by A17, A18; :: thesis: verum

end;

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

take B2 = B2; :: thesis: ( A,A1,B2 are_collinear & B,B1,B2 are_collinear & C,C1,B2 are_collinear )
thus ( A,A1,B2 are_collinear & B,B1,B2 are_collinear & C,C1,B2 are_collinear ) by A28, A14, A15, A16; :: thesis: verum

end;

end;

end;

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

proof

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

suppose A33: B2 <> C2 ; :: thesis: C3,B2,C2 are_collinear

C3,A,A1 are_collinear by A29;
then A34: C3 in Line (A,A1) by Th13, A19;
Line (A,A1) c= Line (B2,C2) by A20, A21, A33, EUCLID_4:43;
hence C3,B2,C2 are_collinear by A33, Th13, A34; :: thesis: verum

end;

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

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

end;

end;

end;

C3 = A2

proof

assume A35: C3 <> A2 ; :: thesis: contradiction
C,A,B is_a_triangle by A1;
then A36: C <> C1 by Th14, A4;
then A37: Line (C,C1) is being_line ;
B,C,A is_a_triangle by A1;
then A38: B <> B1 by Th14, A3;
then A39: Line (B,B1) is being_line ;
C3,B,B1 are_collinear by A30;
then A40: C3 in Line (B,B1) by Th13, A38;
A2,B,B1 are_collinear by A17;
then A41: A2 in Line (B,B1) by Th13, A38;
A2,C,C1 are_collinear by A18;
then A42: A2 in Line (C,C1) by Th13, A36;
C3,C,C1 are_collinear by A31;
then C3 in Line (C,C1) by Th13, A36;
then A43: Line (B,B1) = Line (C,C1) by A40, A35, A41, A42, A39, A37, EUCLID_4:44;
A44: 1 - nu <> 0 by A7;
B in Line (B,B1) by EUCLID_4:41;
then B,C,C1 are_collinear by Th13, A36, A43;
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 A44;
hence contradiction by Th9, A1; :: thesis: verum

end;

hence ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 by A32, Lm7, A1, A2, A3, A4, A5, A6, A7, A22, A23, A24; :: thesis: verum