theorem Th14: :: EUCLID11:19

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