let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies |.(A - B).| = ((((the_diameter_of_the_circumcircle (A,B,C)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((PI / 3) - ((angle (A,C,B)) / 3))) )
assume A1: A,B,C is_a_triangle ; :: thesis: |.(A - B).| = ((((the_diameter_of_the_circumcircle (A,B,C)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((PI / 3) - ((angle (A,C,B)) / 3)))
|.(A - B).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (3 * ((angle (A,C,B)) / 3))) by A1, Lm10;
then |.(A - B).| = (the_diameter_of_the_circumcircle (A,B,C)) * (((4 * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((PI / 3) - ((angle (A,C,B)) / 3)))) by Thm18;
hence |.(A - B).| = ((((the_diameter_of_the_circumcircle (A,B,C)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((PI / 3) - ((angle (A,C,B)) / 3))) ; :: thesis: verum