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

now :: thesis: ( A,B,E are_mutually_distinct & not angle (A,B,E) = PI & not angle (B,E,A) = PI & not angle (E,A,B) = PI )

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

hereby :: thesis: ( not angle (B,E,A) = PI & not angle (E,A,B) = PI )

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

end;

hereby :: thesis: not angle (E,A,B) = PI

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

end;

hereby :: thesis: verum

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

end;

end;

hence A,B,E is_a_triangle by EUCLID_6:20; :: thesis: verum