let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & (angle (B,A,C)) - (angle (C,B,A)) <> PI & (angle (B,A,C)) - (angle (C,B,A)) <> - PI implies cos (((angle (B,A,C)) - (angle (C,B,A))) / 2) <> 0 )
assume that
A1: A,B,C is_a_triangle and
A2: (angle (B,A,C)) - (angle (C,B,A)) <> PI and
A3: (angle (B,A,C)) - (angle (C,B,A)) <> - PI ; :: thesis: cos (((angle (B,A,C)) - (angle (C,B,A))) / 2) <> 0
assume A4: cos (((angle (B,A,C)) - (angle (C,B,A))) / 2) = 0 ; :: thesis: contradiction
consider i0 being Integer such that
A5: ((angle (B,A,C)) - (angle (C,B,A))) / 2 = (PI / 2) + (PI * i0) by A4, BORSUK_7:8;
set a = (angle (B,A,C)) - (angle (C,B,A));
A6: ( 0 <= angle (B,A,C) & angle (B,A,C) < 2 * PI & 0 <= angle (C,B,A) & angle (C,B,A) < 2 * PI ) by EUCLID11:2;
then A7: ( 0 < angle (B,A,C) & angle (B,A,C) < 2 * PI & 0 < angle (C,B,A) & angle (C,B,A) < 2 * PI ) by A1, EUCLID10:30;
A8: 0 - (2 * PI) < (angle (B,A,C)) - (angle (C,B,A)) by A7, XREAL_1:14;
(angle (B,A,C)) - (angle (C,B,A)) < (2 * PI) - 0 by A6, XREAL_1:14;
then ( ((- 2) * PI) / PI < ((1 + (2 * i0)) * PI) / PI & ((1 + (2 * i0)) * PI) / PI < (2 * PI) / PI & PI <> 0 ) by A8, A5, COMPTRIG:5, XREAL_1:74;
then ( (- 2) * (PI / PI) < (1 + (2 * i0)) * (PI / PI) & (1 + (2 * i0)) * (PI / PI) < 2 * (PI / PI) & PI / PI = 1 ) by XCMPLX_1:60;
then ( (- 2) - 1 < (1 + (2 * i0)) - 1 & (1 + (2 * i0)) - 1 < 2 - 1 ) by XREAL_1:14;
then ( (- 3) / 2 < (2 * i0) / 2 & (2 * i0) / 2 < 1 / 2 ) by XREAL_1:74;
then ( i0 = 0 or i0 = - 1 ) by Th2;
hence contradiction by A5, A2, A3; :: thesis: verum