theorem :: EUCLID10:51

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
|.(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)))