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).| = (((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)) & |.(G - F).| = (((4 * (the_diameter_of_the_circumcircle (C,A,B))) * (sin ((angle (C,B,A)) / 3))) * (sin ((angle (B,A,C)) / 3))) * (sin ((angle (A,C,B)) / 3)) & |.(E - G).| = (((4 * (the_diameter_of_the_circumcircle (B,C,A))) * (sin ((angle (B,A,C)) / 3))) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3)) ) )
assume A1: ( 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).| = (((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)) & |.(G - F).| = (((4 * (the_diameter_of_the_circumcircle (C,A,B))) * (sin ((angle (C,B,A)) / 3))) * (sin ((angle (B,A,C)) / 3))) * (sin ((angle (A,C,B)) / 3)) & |.(E - G).| = (((4 * (the_diameter_of_the_circumcircle (B,C,A))) * (sin ((angle (B,A,C)) / 3))) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3)) )
then A2: ( A,B,E is_a_triangle & A,F,C is_a_triangle & C,G,B is_a_triangle ) by Th13, Th14, Th15;

now :: thesis: ( C,A,B is_a_triangle & B,C,A is_a_triangle & C,A,F is_a_triangle & B,C,G is_a_triangle & B,E,A is_a_triangle & angle (C,B,A) < PI & angle (B,A,C) < PI )

thus A3: ( C,A,B is_a_triangle & B,C,A is_a_triangle ) by A1, MENELAUS:15; :: thesis: ( C,A,F is_a_triangle & B,C,G is_a_triangle & B,E,A is_a_triangle & angle (C,B,A) < PI & angle (B,A,C) < PI )
thus ( C,A,F is_a_triangle & B,C,G is_a_triangle & B,E,A is_a_triangle ) by A2, MENELAUS:15; :: thesis: ( angle (C,B,A) < PI & angle (B,A,C) < PI )
angle (A,C,B) <> 0 by A1, EUCLID10:30;
then ( A,C,B are_mutually_distinct & 0 < angle (A,C,B) & angle (A,C,B) < PI ) by A1, A3, EUCLID_6:20, Th2;
hence ( angle (C,B,A) < PI & angle (B,A,C) < PI ) by Th4; :: thesis: verum

end;

hence ( |.(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)) & |.(G - F).| = (((4 * (the_diameter_of_the_circumcircle (C,A,B))) * (sin ((angle (C,B,A)) / 3))) * (sin ((angle (B,A,C)) / 3))) * (sin ((angle (A,C,B)) / 3)) & |.(E - G).| = (((4 * (the_diameter_of_the_circumcircle (B,C,A))) * (sin ((angle (B,A,C)) / 3))) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3)) ) by A1, A2, Th12; :: thesis: verum