let A, B, C, E, F be Point of (TOP-REAL 2); ( 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 implies angle (E,A,F) = (angle (B,A,C)) / 3 )
assume that
A1:
C,A,B is_a_triangle
and
A2:
A,F,C is_a_triangle
and
A3:
F,A,E is_a_triangle
and
A4:
E,A,B is_a_triangle
and
A5:
angle (B,A,E) = (angle (B,A,C)) / 3
and
A6:
angle (F,A,C) = (angle (B,A,C)) / 3
; angle (E,A,F) = (angle (B,A,C)) / 3
A7:
angle (C,A,B) = (2 * PI) - (angle (B,A,C))
by A1, EUCLID10:31;
A8:
( (angle (C,A,F)) + (angle (F,A,E)) = angle (C,A,E) or (angle (C,A,F)) + (angle (F,A,E)) = (angle (C,A,E)) + (2 * PI) )
by EUCLID_6:4;
A9:
( (angle (C,A,E)) + (angle (E,A,B)) = angle (C,A,B) or (angle (C,A,E)) + (angle (E,A,B)) = (angle (C,A,B)) + (2 * PI) )
by EUCLID_6:4;
A10:
angle (C,A,F) = (2 * PI) - ((angle (B,A,C)) / 3)
by A2, A6, EUCLID10:31;
A11:
angle (F,A,E) = (2 * PI) - (angle (E,A,F))
by A3, EUCLID10:31;
A12:
angle (E,A,B) = (2 * PI) - ((angle (B,A,C)) / 3)
by A5, A4, EUCLID10:31;
A13:
not angle (E,A,F) = (4 * PI) + ((angle (B,A,C)) / 3)
proof
assume A14:
angle (
E,
A,
F)
= (4 * PI) + ((angle (B,A,C)) / 3)
;
contradiction
now ( 2 * PI < 4 * PI & 0 < (angle (B,A,C)) / 3 )
0 + (2 * PI) < (2 * PI) + (2 * PI)
by COMPTRIG:5, XREAL_1:8;
hence
2
* PI < 4
* PI
;
0 < (angle (B,A,C)) / 3
(
0 <= angle (
B,
A,
C) &
angle (
B,
A,
C)
<> 0 )
by Th2, A1, EUCLID10:30;
hence
0 < (angle (B,A,C)) / 3
;
verum end;
then
(2 * PI) + 0 < (4 * PI) + ((angle (B,A,C)) / 3)
by XREAL_1:8;
hence
contradiction
by A14, Th2;
verum
end;
not angle (E,A,F) = (2 * PI) + ((angle (B,A,C)) / 3)
proof
assume A15:
angle (
E,
A,
F)
= (2 * PI) + ((angle (B,A,C)) / 3)
;
contradiction
(
0 <= angle (
B,
A,
C) &
angle (
B,
A,
C)
<> 0 )
by Th2, A1, EUCLID10:30;
then
(2 * PI) + 0 < (2 * PI) + ((angle (B,A,C)) / 3)
by XREAL_1:8;
hence
contradiction
by A15, Th2;
verum
end;
hence
angle (E,A,F) = (angle (B,A,C)) / 3
by A12, A7, A8, A9, A10, A11, A13; verum