let A, B, C be Point of (TOP-REAL 2); ( A,C,B is_a_triangle implies sin ((PI / 3) - ((angle (A,C,B)) / 3)) <> 0 )
assume A1:
A,C,B is_a_triangle
; sin ((PI / 3) - ((angle (A,C,B)) / 3)) <> 0
assume
sin ((PI / 3) - ((angle (A,C,B)) / 3)) = 0
; 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; verum