theorem Th12: :: EUCLID11:17

for A, B, C, E, F being Point of (TOP-REAL 2) st A,B,C is_a_triangle & A,B,E is_a_triangle & angle (E,B,A) = (angle (C,B,A)) / 3 & angle (B,A,E) = (angle (B,A,C)) / 3 & A,F,C is_a_triangle & angle (A,C,F) = (angle (A,C,B)) / 3 & angle (F,A,C) = (angle (B,A,C)) / 3 & angle (A,C,B) < PI holds
|.(F - E).| = (((4 * (the_diameter_of_the_circumcircle (A,B,C))) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3))) * (sin ((angle (B,A,C)) / 3))