theorem Th15: :: EUCLID11:20

for A, B, C, G being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (C,B,G) = (angle (C,B,A)) / 3 & angle (G,C,B) = (angle (A,C,B)) / 3 holds
C,G,B is_a_triangle