let A, B, C, F be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & A,F,C is_a_triangle & angle (C,F,A) < PI & angle (A,C,F) = (angle (A,C,B)) / 3 & angle (F,A,C) = (angle (B,A,C)) / 3 & (((angle (A,C,B)) / 3) + ((angle (B,A,C)) / 3)) + ((angle (C,B,A)) / 3) = PI / 3 & sin ((PI / 3) - ((angle (C,B,A)) / 3)) <> 0 implies |.(A - F).| = (((4 * (the_diameter_of_the_circumcircle (A,B,C))) * (sin ((angle (C,B,A)) / 3))) * (sin ((PI / 3) + ((angle (C,B,A)) / 3)))) * (sin ((angle (A,C,B)) / 3)) )
assume that
A1: A,B,C is_a_triangle and
A2: A,F,C is_a_triangle and
A3: angle (C,F,A) < PI and
A4: angle (A,C,F) = (angle (A,C,B)) / 3 and
A5: angle (F,A,C) = (angle (B,A,C)) / 3 and
A6: (((angle (A,C,B)) / 3) + ((angle (B,A,C)) / 3)) + ((angle (C,B,A)) / 3) = PI / 3 and
A7: sin ((PI / 3) - ((angle (C,B,A)) / 3)) <> 0 ; :: thesis: |.(A - F).| = (((4 * (the_diameter_of_the_circumcircle (A,B,C))) * (sin ((angle (C,B,A)) / 3))) * (sin ((PI / 3) + ((angle (C,B,A)) / 3)))) * (sin ((angle (A,C,B)) / 3))
A8: |.(A - F).| * (sin ((PI / 3) - ((angle (C,B,A)) / 3))) = |.(A - C).| * (sin ((angle (A,C,B)) / 3)) by A3, A4, A5, A2, A6, Th7
.= |.(C - A).| * (sin ((angle (A,C,B)) / 3)) by EUCLID_6:43
.= ((the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (C,B,A)))) * (sin ((angle (A,C,B)) / 3)) by A1, EUCLID10:50 ;
sin (angle (C,B,A)) = sin (3 * ((angle (C,B,A)) / 3))
.= ((4 * (sin ((angle (C,B,A)) / 3))) * (sin ((PI / 3) + ((angle (C,B,A)) / 3)))) * (sin ((PI / 3) - ((angle (C,B,A)) / 3))) by EUCLID10:29 ;
then |.(A - F).| = ((((((the_diameter_of_the_circumcircle (A,B,C)) * 4) * (sin ((angle (C,B,A)) / 3))) * (sin ((PI / 3) + ((angle (C,B,A)) / 3)))) * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) - ((angle (C,B,A)) / 3)))) / (sin ((PI / 3) - ((angle (C,B,A)) / 3))) by A7, A8, XCMPLX_1:89;
then A9: |.(A - F).| = (((((the_diameter_of_the_circumcircle (A,B,C)) * 4) * (sin ((angle (C,B,A)) / 3))) * (sin ((PI / 3) + ((angle (C,B,A)) / 3)))) * (sin ((angle (A,C,B)) / 3))) * ((sin ((PI / 3) - ((angle (C,B,A)) / 3))) / (sin ((PI / 3) - ((angle (C,B,A)) / 3)))) ;
(sin ((PI / 3) - ((angle (C,B,A)) / 3))) / (sin ((PI / 3) - ((angle (C,B,A)) / 3))) = 1 by A7, XCMPLX_1:60;
hence |.(A - F).| = (((4 * (the_diameter_of_the_circumcircle (A,B,C))) * (sin ((angle (C,B,A)) / 3))) * (sin ((PI / 3) + ((angle (C,B,A)) / 3)))) * (sin ((angle (A,C,B)) / 3)) by A9; :: thesis: verum