let A, B, C, E, F, G be Point of (TOP-REAL 2); ( A,B,C is_a_triangle & angle (A,B,C) < PI & angle (E,C,A) = (angle (B,C,A)) / 3 & angle (C,A,E) = (angle (C,A,B)) / 3 & angle (A,B,F) = (angle (A,B,C)) / 3 & angle (F,A,B) = (angle (C,A,B)) / 3 & angle (B,C,G) = (angle (B,C,A)) / 3 & angle (G,B,C) = (angle (A,B,C)) / 3 implies ( |.(F - E).| = |.(G - F).| & |.(F - E).| = |.(E - G).| & |.(G - F).| = |.(E - G).| ) )
assume A1:
( A,B,C is_a_triangle & angle (A,B,C) < PI & angle (E,C,A) = (angle (B,C,A)) / 3 & angle (C,A,E) = (angle (C,A,B)) / 3 & angle (A,B,F) = (angle (A,B,C)) / 3 & angle (F,A,B) = (angle (C,A,B)) / 3 & angle (B,C,G) = (angle (B,C,A)) / 3 & angle (G,B,C) = (angle (A,B,C)) / 3 )
; ( |.(F - E).| = |.(G - F).| & |.(F - E).| = |.(E - G).| & |.(G - F).| = |.(E - G).| )
A,C,B is_a_triangle
by A1, MENELAUS:15;
hence
( |.(F - E).| = |.(G - F).| & |.(F - E).| = |.(E - G).| & |.(G - F).| = |.(E - G).| )
by A1, Th17; verum