let A, B, C be Point of (TOP-REAL 2); :: thesis: ( angle (B,A,C) <> angle (C,B,A) implies sin (((angle (B,A,C)) - (angle (C,B,A))) / 2) <> 0 )
assume A1: angle (B,A,C) <> angle (C,B,A) ; :: thesis: sin (((angle (B,A,C)) - (angle (C,B,A))) / 2) <> 0
assume A2: sin (((angle (B,A,C)) - (angle (C,B,A))) / 2) = 0 ; :: thesis: contradiction
then consider i0 being Integer such that
A3: ((angle (B,A,C)) - (angle (C,B,A))) / 2 = PI * i0 by BORSUK_7:7;
set a = (angle (B,A,C)) - (angle (C,B,A));
A4: ( 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;
A5: 0 - (2 * PI) < 0 - (angle (C,B,A)) by EUCLID11:2, XREAL_1:10;
per cases ( i0 = 0 or i0 < 0 or i0 > 0 ) ;
suppose i0 = 0 ; :: thesis: contradiction
hence contradiction by A3, A1; :: thesis: verum
end;
suppose A6: i0 < 0 ; :: thesis: contradiction
PI in ].0,4.[ by SIN_COS:def 28;
then 0 < PI by XXREAL_1:4;
then A7: (angle (B,A,C)) - (angle (C,B,A)) < 0 by A3, A6;
- (2 * PI) < (angle (B,A,C)) - (angle (C,B,A)) by A5, EUCLID11:2, XREAL_1:8;
hence contradiction by A2, A7, Th5; :: thesis: verum
end;
suppose A8: i0 > 0 ; :: thesis: contradiction
( 0 < (angle (B,A,C)) - (angle (C,B,A)) & (angle (B,A,C)) - (angle (C,B,A)) < 2 * PI )
proof
thus 0 < (angle (B,A,C)) - (angle (C,B,A)) by A3, A8, COMPTRIG:5; :: thesis: (angle (B,A,C)) - (angle (C,B,A)) < 2 * PI
(angle (B,A,C)) - (angle (C,B,A)) < (2 * PI) - 0 by A4, XREAL_1:14;
hence (angle (B,A,C)) - (angle (C,B,A)) < 2 * PI ; :: thesis: verum
end;
hence contradiction by A2, Th4; :: thesis: verum
end;
end;