let A, B, C, E, F, G be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & angle (A,C,B) < PI & angle (E,B,A) = (angle (C,B,A)) / 3 & angle (B,A,E) = (angle (B,A,C)) / 3 & angle (A,C,F) = (angle (A,C,B)) / 3 & angle (F,A,C) = (angle (B,A,C)) / 3 & angle (C,B,G) = (angle (C,B,A)) / 3 & angle (G,C,B) = (angle (A,C,B)) / 3 implies ( |.(F - E).| = |.(G - F).| & |.(F - E).| = |.(E - G).| & |.(G - F).| = |.(E - G).| ) )
assume ( A,B,C is_a_triangle & angle (A,C,B) < PI & angle (E,B,A) = (angle (C,B,A)) / 3 & angle (B,A,E) = (angle (B,A,C)) / 3 & angle (A,C,F) = (angle (A,C,B)) / 3 & angle (F,A,C) = (angle (B,A,C)) / 3 & angle (C,B,G) = (angle (C,B,A)) / 3 & angle (G,C,B) = (angle (A,C,B)) / 3 ) ; :: thesis: ( |.(F - E).| = |.(G - F).| & |.(F - E).| = |.(E - G).| & |.(G - F).| = |.(E - G).| )
then A1: ( |.(F - E).| = ((((the_diameter_of_the_circumcircle (A,B,C)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3))) * (sin ((angle (B,A,C)) / 3)) & |.(G - F).| = ((((the_diameter_of_the_circumcircle (C,A,B)) * 4) * (sin ((angle (C,B,A)) / 3))) * (sin ((angle (B,A,C)) / 3))) * (sin ((angle (A,C,B)) / 3)) & |.(E - G).| = ((((the_diameter_of_the_circumcircle (B,C,A)) * 4) * (sin ((angle (B,A,C)) / 3))) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3)) ) by Th16;
( the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (C,A,B) & the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (B,C,A) ) by EUCLID10:46;
hence ( |.(F - E).| = |.(G - F).| & |.(F - E).| = |.(E - G).| & |.(G - F).| = |.(E - G).| ) by A1; :: thesis: verum