let A, B, C, G be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & angle (C,B,G) = (angle (C,B,A)) / 3 & angle (G,C,B) = (angle (A,C,B)) / 3 implies C,G,B is_a_triangle )
assume that
A1: A,B,C is_a_triangle and
A2: angle (C,B,G) = (angle (C,B,A)) / 3 and
A3: angle (G,C,B) = (angle (A,C,B)) / 3 ; :: thesis: C,G,B is_a_triangle
A4: A,B,C are_mutually_distinct by A1, EUCLID_6:20;
A5: ( angle (A,C,B) <> 0 & angle (C,B,A) <> 0 ) by A1, EUCLID10:30;

now :: thesis: ( C,G,B are_mutually_distinct & not angle (C,G,B) = PI & not angle (G,B,C) = PI & not angle (B,C,G) = PI )

thus C,G,B are_mutually_distinct by A2, A3, A4, A5, Th1; :: thesis: ( not angle (C,G,B) = PI & not angle (G,B,C) = PI & not angle (B,C,G) = PI )

hereby :: thesis: ( not angle (G,B,C) = PI & not angle (B,C,G) = PI )

assume angle (C,G,B) = PI ; :: thesis: contradiction
then ( G in LSeg (C,B) & G <> C ) by A2, A5, Th1, EUCLID_6:11;
then angle (G,C,B) = angle (B,C,B) by EUCLID_6:9
.= 0 by Th1 ;
hence contradiction by A3, A1, EUCLID10:30; :: thesis: verum

end;

hereby :: thesis: not angle (B,C,G) = PI

assume angle (G,B,C) = PI ; :: thesis: contradiction
then A6: angle (C,B,G) = (2 * PI) - PI by COMPTRIG:5, EUCLID_3:37
.= PI ;
(2 * PI) + 0 < (2 * PI) + PI by COMPTRIG:5, XREAL_1:8;
hence contradiction by A2, A6, Th2; :: thesis: verum

end;

hereby :: thesis: verum

assume angle (B,C,G) = PI ; :: thesis: contradiction
then A7: angle (G,C,B) = (2 * PI) - PI by COMPTRIG:5, EUCLID_3:37
.= PI ;
(2 * PI) + 0 < (2 * PI) + PI by COMPTRIG:5, XREAL_1:8;
hence contradiction by A3, A7, Th2; :: thesis: verum

end;

end;

hence C,G,B is_a_triangle by EUCLID_6:20; :: thesis: verum