theorem Th9: :: EUCLID11:14

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