theorem Th10: :: EUCLID11:15

for A, B, C, E, F being Point of (TOP-REAL 2) st C,A,B is_a_triangle & angle (A,C,B) < PI & 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
(((PI / 3) + ((angle (A,C,B)) / 3)) + ((PI / 3) + ((angle (C,B,A)) / 3))) + (angle (E,A,F)) = PI