let A, B, C, E, F be Point of (TOP-REAL 2); :: thesis: ( 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 implies (((PI / 3) + ((angle (A,C,B)) / 3)) + ((PI / 3) + ((angle (C,B,A)) / 3))) + (angle (E,A,F)) = PI )
assume that
A1: C,A,B is_a_triangle and
A2: angle (A,C,B) < PI and
A3: A,F,C is_a_triangle and
A4: F,A,E is_a_triangle and
A5: E,A,B is_a_triangle and
A6: angle (B,A,E) = (angle (B,A,C)) / 3 and
A7: angle (F,A,C) = (angle (B,A,C)) / 3 ; :: thesis: (((PI / 3) + ((angle (A,C,B)) / 3)) + ((PI / 3) + ((angle (C,B,A)) / 3))) + (angle (E,A,F)) = PI
set lambda = (((PI / 3) + ((angle (A,C,B)) / 3)) + ((PI / 3) + ((angle (C,B,A)) / 3))) + (angle (E,A,F));
set theta = (((angle (A,C,B)) / 3) + ((angle (C,B,A)) / 3)) + ((angle (B,A,C)) / 3);
A8: angle (E,A,F) = (angle (B,A,C)) / 3 by A1, A3, A4, A5, A6, A7, Th9;
( C,A,B are_mutually_distinct & angle (A,C,B) < PI ) by A1, A2, EUCLID_6:20;
then ((angle (A,C,B)) + (angle (C,B,A))) + (angle (B,A,C)) = PI by EUCLID_3:47;
hence (((PI / 3) + ((angle (A,C,B)) / 3)) + ((PI / 3) + ((angle (C,B,A)) / 3))) + (angle (E,A,F)) = PI by A8; :: thesis: verum