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 & ( not (1 - mu) + (lambda * mu) <> 0 or not (1 - lambda) + (nu * lambda) <> 0 or not (1 - nu) + (mu * nu) <> 0 ) holds
( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff ( 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) ) )
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 & ( not (1 - mu) + (lambda * mu) <> 0 or not (1 - lambda) + (nu * lambda) <> 0 or not (1 - nu) + (mu * nu) <> 0 ) implies ( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff ( 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) ) ) )
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: ( not (1 - mu) + (lambda * mu) <> 0 or not (1 - lambda) + (nu * lambda) <> 0 or not (1 - nu) + (mu * nu) <> 0 ) ; :: thesis: ( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff ( 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) ) )
A9: B,C,A is_a_triangle by Th15, A1;
A10: C,A,B is_a_triangle by Th15, A1;

hereby :: thesis: ( 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) implies ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 )

assume ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 ; :: thesis: ( 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) )
then B1: 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) by Lm4, A5, A6, A7;
then B2: 0 = ((nu * lambda) * mu) - (((1 - nu) * (1 - lambda)) * (1 - mu)) ;
B3: 0 = ((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda)) by B1;
( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 )

proof

per cases ( (1 - mu) + (lambda * mu) = 0 or (1 - lambda) + (nu * lambda) = 0 or (1 - nu) + (mu * nu) = 0 ) by A8;

suppose H0: (1 - mu) + (lambda * mu) = 0 ; :: thesis: ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 )

then (1 - lambda) + (nu * lambda) = 0 by Lm6, A6, B1;
hence ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 ) by Lm6, A5, B2, H0; :: thesis: verum

end;

suppose H1: (1 - lambda) + (nu * lambda) = 0 ; :: thesis: ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 )

then (1 - nu) + (nu * mu) = 0 by Lm6, A5, B2;
hence ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 ) by Lm6, A7, B3, H1; :: thesis: verum

end;

suppose H2: (1 - nu) + (mu * nu) = 0 ; :: thesis: ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 )

then (1 - mu) + (lambda * mu) = 0 by Lm6, A7, B3;
hence ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 ) by Lm6, A6, B1, H2; :: thesis: verum

end;

end;

end;

hence ( 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 A1, A9, Th18, A2, A3, A4, A5, A6, A7, A10; :: thesis: verum

end;

assume ( Line (A,A1) is_parallel_to Line (B,B1) & Line (B,B1) is_parallel_to Line (C,C1) ) ; :: thesis: ( not Line (C,C1) is_parallel_to Line (A,A1) or ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 )
then B4: ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 ) by A1, A9, Th18, A2, A3, A4, A6, A7;
then ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (- (mu * nu)))
.= ((lambda + ((1 - lambda) * (1 - mu))) * mu) * nu
.= 0 by B4 ;
hence ( not Line (C,C1) is_parallel_to Line (A,A1) or ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 ) by Lm4, A5, A6, A7; :: thesis: verum