let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,C,B is_a_triangle implies sin ((PI / 3) - ((angle (A,C,B)) / 3)) <> 0 )
assume A1: A,C,B is_a_triangle ; :: thesis: sin ((PI / 3) - ((angle (A,C,B)) / 3)) <> 0
assume sin ((PI / 3) - ((angle (A,C,B)) / 3)) = 0 ; :: thesis: contradiction
then consider i0 being Integer such that
A2: (PI / 3) - ((angle (A,C,B)) / 3) = PI * i0 by BORSUK_7:7;
( 0 + ((3 * i0) * PI) <= (PI - ((3 * i0) * PI)) + ((3 * i0) * PI) & (PI - ((3 * i0) * PI)) + ((3 * i0) * PI) < (2 * PI) + ((3 * i0) * PI) ) by A2, XREAL_1:6, Th2;
then ( (3 * i0) * PI <= PI & PI - PI < ((2 * PI) + ((3 * i0) * PI)) - PI ) by XREAL_1:9;
then ( ((3 * i0) * PI) / PI <= PI / PI & 0 < (1 + (3 * i0)) * PI ) by COMPTRIG:5, XREAL_1:72;
then ( (3 * i0) * (PI / PI) <= PI / PI & 0 / PI < ((1 + (3 * i0)) * PI) / PI ) by COMPTRIG:5;
then ( 3 * i0 <= PI / PI & 0 / PI < 1 + (3 * i0) ) by XCMPLX_1:88, COMPTRIG:5;
then ( 3 * i0 <= 1 & 0 < 1 + (3 * i0) ) by XCMPLX_1:60;
then i0 = 0 by Lm4;
hence contradiction by A1, A2, EUCLID_6:20; :: thesis: verum