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

now :: thesis: ( A,F,C are_mutually_distinct & not angle (A,F,C) = PI & not angle (C,A,F) = PI & not angle (F,C,A) = PI )

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

hereby :: thesis: ( not angle (C,A,F) = PI & not angle (F,C,A) = PI )

assume angle (A,F,C) = PI ; :: thesis: contradiction
then ( F in LSeg (A,C) & F <> A ) by A2, A5, Th1, EUCLID_6:11;
then angle (C,A,F) = angle (F,A,F) by EUCLID_6:9
.= 0 by Th1 ;
hence contradiction by A5, A3, EUCLID_3:36; :: thesis: verum

end;

hereby :: thesis: not angle (F,C,A) = PI

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

end;

hereby :: thesis: verum

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

end;

end;

hence A,F,C is_a_triangle by EUCLID_6:20; :: thesis: verum