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
( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent )
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 ( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent ) )
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 ; :: thesis: ( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent )
A8: A <> A1 by Th14, A1, A2;
A9: B,C,A is_a_triangle by A1;
then A10: B <> B1 by Th14, A3;
A11: C,A,B is_a_triangle by A1;
then A12: C <> C1 by Th14, A4;

hereby :: thesis: ( Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent implies ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 )

assume A13: ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 ; :: thesis: Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent

per cases ( ( (1 - mu) + (lambda * mu) <> 0 & (1 - lambda) + (nu * lambda) <> 0 & (1 - nu) + (mu * nu) <> 0 ) or not (1 - mu) + (lambda * mu) <> 0 or not (1 - lambda) + (nu * lambda) <> 0 or not (1 - nu) + (mu * nu) <> 0 ) ;

suppose ( (1 - mu) + (lambda * mu) <> 0 & (1 - lambda) + (nu * lambda) <> 0 & (1 - nu) + (mu * nu) <> 0 ) ; :: thesis: Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent

then consider A2 being Point of (TOP-REAL 2) such that
A14: ( A,A1,A2 are_collinear & B,B1,A2 are_collinear & C,C1,A2 are_collinear ) by A13, Th21, A1, A2, A3, A4, A5, A6, A7;
( A2,A,A1 are_collinear & A2,B,B1 are_collinear & A2,C,C1 are_collinear ) by A14;
then ( A2 in Line (A,A1) & A2 in Line (B,B1) & A2 in Line (C,C1) ) by Th13, A8, A10, A12;
hence Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent ; :: thesis: verum

end;

suppose ( not (1 - mu) + (lambda * mu) <> 0 or not (1 - lambda) + (nu * lambda) <> 0 or not (1 - nu) + (mu * nu) <> 0 ) ; :: thesis: Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent

then ( Line (A,A1) is_parallel_to Line (B,B1) & Line (B,B1) is_parallel_to Line (C,C1) & Line (C,C1) is_parallel_to Line (A,A1) ) by A13, Lm6, A1, A2, A3, A4, A5, A6, A7;
hence Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent ; :: thesis: verum

end;

end;

end;

assume Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent ; :: thesis: ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1

per cases then ( ( Line (A,A1) is_parallel_to Line (B,B1) & Line (B,B1) is_parallel_to Line (C,C1) & Line (C,C1) is_parallel_to Line (A,A1) ) or ex C2 being Point of (TOP-REAL 2) st
( C2 in Line (A,A1) & C2 in Line (B,B1) & C2 in Line (C,C1) ) ) ;

suppose A15: ( Line (A,A1) is_parallel_to Line (B,B1) & Line (B,B1) is_parallel_to Line (C,C1) & Line (C,C1) is_parallel_to Line (A,A1) ) ; :: thesis: ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1

then ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 ) by Th16, A1, A9, A11, A2, A3, A4, A5, A6, A7;
hence ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 by Lm6, A15, A1, A2, A3, A4, A5, A6, A7; :: thesis: verum

end;

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

then consider C2 being Point of (TOP-REAL 2) such that
A16: ( C2 in Line (A,A1) & C2 in Line (B,B1) & C2 in Line (C,C1) ) ;
( not Line (A,A1) is_parallel_to Line (B,B1) & not Line (B,B1) is_parallel_to Line (C,C1) & not Line (C,C1) is_parallel_to Line (A,A1) ) by A16, XBOOLE_0:3;
then A17: ( (1 - mu) + (lambda * mu) <> 0 & (1 - nu) + (mu * nu) <> 0 & (1 - lambda) + (nu * lambda) <> 0 ) by Th16, A1, A2, A3, A4, A5, A6, A7, A9, A11;
( C2,A,A1 are_collinear & C2,B,B1 are_collinear & C2,C,C1 are_collinear ) by A16, Th13, A8, A10, A12;
then ( A,A1,C2 are_collinear & B,B1,C2 are_collinear & C,C1,C2 are_collinear ) ;
hence ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 by A17, Th21, A1, A2, A3, A4, A5, A6, A7; :: thesis: verum

end;

end;