let A, B, C, E, F be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & A,B,E is_a_triangle & angle (E,B,A) = (angle (C,B,A)) / 3 & angle (B,A,E) = (angle (B,A,C)) / 3 & A,F,C is_a_triangle & angle (A,C,F) = (angle (A,C,B)) / 3 & angle (F,A,C) = (angle (B,A,C)) / 3 & angle (A,C,B) < PI implies |.(F - E).| = (((4 * (the_diameter_of_the_circumcircle (A,B,C))) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3))) * (sin ((angle (B,A,C)) / 3)) )
assume that
A1: A,B,C is_a_triangle and
A2: A,B,E is_a_triangle and
A3: angle (E,B,A) = (angle (C,B,A)) / 3 and
A4: angle (B,A,E) = (angle (B,A,C)) / 3 and
A5: A,F,C is_a_triangle and
A6: angle (A,C,F) = (angle (A,C,B)) / 3 and
A7: angle (F,A,C) = (angle (B,A,C)) / 3 and
A8: angle (A,C,B) < PI ; :: thesis: |.(F - E).| = (((4 * (the_diameter_of_the_circumcircle (A,B,C))) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3))) * (sin ((angle (B,A,C)) / 3))
A9: A,C,B is_a_triangle by A1, MENELAUS:15;
then A10: sin ((PI / 3) - ((angle (A,C,B)) / 3)) <> 0 by Th11;
C,B,A is_a_triangle by A1, MENELAUS:15;
then A11: sin ((PI / 3) - ((angle (C,B,A)) / 3)) <> 0 by Th11;
A12: A,C,B are_mutually_distinct by A9, EUCLID_6:20;
then ((angle (A,C,B)) + (angle (C,B,A))) + (angle (B,A,C)) = PI by A8, EUCLID_3:47;
then A13: (((angle (A,C,B)) / 3) + ((angle (B,A,C)) / 3)) + ((angle (C,B,A)) / 3) = PI / 3 ;
angle (A,C,B) <> 0 by A1, EUCLID10:30;
then A14: 0 < angle (A,C,B) by Th2;
then A15: angle (C,B,A) < PI by A12, A8, Th4;
angle (A,C,B) <> 0 by A1, EUCLID10:30;
then A16: ( 0 < angle (A,C,B) & angle (A,C,B) < PI & A,C,B are_mutually_distinct ) by A9, EUCLID_6:20, A8, Th2;
then angle (B,A,C) < PI by Th4;
then A17: ( (angle (B,A,C)) / 3 < PI / 3 & PI / 3 < PI ) by XREAL_1:74, XREAL_1:221, COMPTRIG:5;
A18: ( E,A,B is_a_triangle & B,A,E is_a_triangle & E,B,A is_a_triangle ) by A2, MENELAUS:15;
then A19: ( B,A,E are_mutually_distinct & E,B,A are_mutually_distinct & angle (E,B,A) <> 0 & angle (B,A,E) <> 0 ) by EUCLID_6:20, EUCLID10:30;
( 0 < angle (B,A,E) & angle (B,A,E) < PI ) by A17, A4, XXREAL_0:2, A19, Th2;
then A20: angle (A,E,B) < PI by A19, Th4;
F,A,C is_a_triangle by A5, MENELAUS:15;
then A21: ( F,A,C are_mutually_distinct & angle (F,A,C) <> 0 ) by EUCLID_6:20, EUCLID10:30;
then ( 0 < angle (F,A,C) & angle (F,A,C) < PI ) by A17, A7, XXREAL_0:2, Th2;
then A22: angle (C,F,A) < PI by A21, Th4;
A23: F,A,E is_a_triangle

proof

now :: thesis: ( F,A,E are_mutually_distinct & angle (F,A,E) <> PI & angle (A,E,F) <> PI & angle (E,F,A) <> PI )

E <> F

proof

assume A24: E = F ; :: thesis: contradiction

per cases ( (angle (B,A,E)) + (angle (E,A,C)) = angle (B,A,C) or (angle (B,A,E)) + (angle (E,A,C)) = (angle (B,A,C)) + (2 * PI) ) by EUCLID_6:4;

suppose A25: (angle (B,A,E)) + (angle (E,A,C)) = angle (B,A,C) ; :: thesis: contradiction

A26: 0 < angle (B,A,C) by A16, Th4;
then A27: (angle (B,A,C)) / (angle (B,A,C)) = 1 by XCMPLX_1:60;
(angle (B,A,C)) / (angle (B,A,C)) = ((2 / 3) * (angle (B,A,C))) / (angle (B,A,C)) by A24, A7, A4, A25
.= 2 / 3 by A27 ;
hence contradiction by A26, XCMPLX_1:60; :: thesis: verum

end;

suppose A28: (angle (B,A,E)) + (angle (E,A,C)) = (angle (B,A,C)) + (2 * PI) ; :: thesis: contradiction

A29: 0 < angle (B,A,C) by A16, Th4;
2 * PI = - ((1 / 3) * (angle (B,A,C))) by A24, A7, A4, A28;
hence contradiction by A29, COMPTRIG:5; :: thesis: verum

end;

end;

end;

hence F,A,E are_mutually_distinct by A21, A19; :: thesis: ( angle (F,A,E) <> PI & angle (A,E,F) <> PI & angle (E,F,A) <> PI )

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

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

assume A30: angle (F,A,E) = PI ; :: thesis: contradiction
A31: ( (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;

per cases ( (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;

suppose (angle (C,A,E)) + (angle (E,A,B)) = angle (C,A,B) ; :: thesis: contradiction

per cases then ( ((angle (C,A,F)) + PI) + (angle (E,A,B)) = angle (C,A,B) or ((angle (C,A,F)) - PI) + (angle (E,A,B)) = angle (C,A,B) ) by A31, A30;

suppose A32: ((angle (C,A,F)) + PI) + (angle (E,A,B)) = angle (C,A,B) ; :: thesis: contradiction

A33: 0 < angle (B,A,C) by A16, Th4;
A34: ((angle (C,A,F)) + PI) + (angle (E,A,B)) = (2 * PI) - (angle (B,A,C)) by A32, A1, EUCLID10:31;
A35: angle (C,A,F) = (2 * PI) - ((angle (B,A,C)) / 3) by A7, A5, EUCLID10:31;
( angle (E,A,B) = (2 * PI) - (angle (B,A,E)) & (2 * PI) - (angle (B,A,E)) = (2 * PI) - ((angle (B,A,C)) / 3) ) by A4, A2, EUCLID10:31;
then 3 * PI = - ((1 / 3) * (angle (B,A,C))) by A34, A35;
hence contradiction by A33, COMPTRIG:5; :: thesis: verum

end;

suppose A36: ((angle (C,A,F)) - PI) + (angle (E,A,B)) = angle (C,A,B) ; :: thesis: contradiction

A37: 0 < angle (B,A,C) by A16, Th4;
A38: ((angle (C,A,F)) - PI) + (angle (E,A,B)) = (2 * PI) - (angle (B,A,C)) by A36, A1, EUCLID10:31;
A39: ( angle (C,A,F) = (2 * PI) - (angle (F,A,C)) & (2 * PI) - (angle (F,A,C)) = (2 * PI) - ((angle (B,A,C)) / 3) ) by A7, A5, EUCLID10:31;
angle (E,A,B) = (2 * PI) - ((angle (B,A,C)) / 3) by A4, A2, EUCLID10:31;
hence contradiction by A37, COMPTRIG:5, A38, A39; :: thesis: verum

end;

end;

end;

suppose (angle (C,A,E)) + (angle (E,A,B)) = (angle (C,A,B)) + (2 * PI) ; :: thesis: contradiction

per cases then ( ((angle (C,A,F)) + PI) + (angle (E,A,B)) = (angle (C,A,B)) + (2 * PI) or ((angle (C,A,F)) - PI) + (angle (E,A,B)) = (angle (C,A,B)) + (2 * PI) ) by A31, A30;

suppose A40: ((angle (C,A,F)) + PI) + (angle (E,A,B)) = (angle (C,A,B)) + (2 * PI) ; :: thesis: contradiction

A41: 0 < angle (B,A,C) by A16, Th4;
A42: ((angle (C,A,F)) + PI) + (angle (E,A,B)) = ((2 * PI) - (angle (B,A,C))) + (2 * PI) by A40, A1, EUCLID10:31;
A43: angle (C,A,F) = (2 * PI) - ((angle (B,A,C)) / 3) by A7, A5, EUCLID10:31;
angle (E,A,B) = (2 * PI) - ((angle (B,A,C)) / 3) by A4, A2, EUCLID10:31;
hence contradiction by A42, A43, A41, COMPTRIG:5; :: thesis: verum

end;

suppose A44: ((angle (C,A,F)) - PI) + (angle (E,A,B)) = (angle (C,A,B)) + (2 * PI) ; :: thesis: contradiction

A45: ((angle (C,A,F)) - PI) + (angle (E,A,B)) = ((2 * PI) - (angle (B,A,C))) + (2 * PI) by A44, A1, EUCLID10:31;
A46: angle (C,A,F) = (2 * PI) - ((angle (B,A,C)) / 3) by A7, A5, EUCLID10:31;
angle (E,A,B) = (2 * PI) - ((angle (B,A,C)) / 3) by A4, A2, EUCLID10:31;
then ( 3 * PI = ((3 * 1) / 3) * (angle (B,A,C)) & (2 * PI) + 0 < (2 * PI) + PI ) by A45, A46, XREAL_1:6, COMPTRIG:5;
hence contradiction by Th2; :: thesis: verum

end;

end;

end;

end;

end;

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

assume angle (A,E,F) = PI ; :: thesis: contradiction
then A47: ( E in LSeg (A,F) & E <> A ) by A19, EUCLID_6:11;
A48: ( (angle (C,A,F)) + (angle (F,A,B)) = angle (C,A,B) or (angle (C,A,F)) + (angle (F,A,B)) = (angle (C,A,B)) + (2 * PI) ) by EUCLID_6:4;
A49: angle (C,A,F) = (2 * PI) - ((angle (B,A,C)) / 3) by A7, A5, EUCLID10:31;
angle (F,A,B) = angle (E,A,B) by A47, EUCLID_6:9
.= (2 * PI) - ((angle (B,A,C)) / 3) by A4, A2, EUCLID10:31 ;

per cases then ( (((2 * PI) - ((angle (B,A,C)) / 3)) + (2 * PI)) - ((angle (B,A,C)) / 3) = (2 * PI) - (angle (B,A,C)) or (((2 * PI) - ((angle (B,A,C)) / 3)) + (2 * PI)) - ((angle (B,A,C)) / 3) = ((2 * PI) - (angle (B,A,C))) + (2 * PI) ) by A1, EUCLID10:31, A48, A49;

suppose A50: (((2 * PI) - ((angle (B,A,C)) / 3)) + (2 * PI)) - ((angle (B,A,C)) / 3) = (2 * PI) - (angle (B,A,C)) ; :: thesis: contradiction

0 < angle (B,A,C) by A16, Th4;
hence contradiction by A50, COMPTRIG:5; :: thesis: verum

end;

suppose (((2 * PI) - ((angle (B,A,C)) / 3)) + (2 * PI)) - ((angle (B,A,C)) / 3) = ((2 * PI) - (angle (B,A,C))) + (2 * PI) ; :: thesis: contradiction

hence contradiction by A16, Th4; :: thesis: verum

end;

end;

end;

hereby :: thesis: verum

assume angle (E,F,A) = PI ; :: thesis: contradiction
then A51: ( F in LSeg (E,A) & F <> A ) by A21, EUCLID_6:11;
A52: ( (angle (C,A,F)) + (angle (F,A,B)) = angle (C,A,B) or (angle (C,A,F)) + (angle (F,A,B)) = (angle (C,A,B)) + (2 * PI) ) by EUCLID_6:4;
A53: angle (C,A,F) = (2 * PI) - ((angle (B,A,C)) / 3) by A5, A7, EUCLID10:31;
angle (F,A,B) = angle (E,A,B) by A51, EUCLID_6:9
.= (2 * PI) - ((angle (B,A,C)) / 3) by A4, A2, EUCLID10:31 ;

per cases then ( (((2 * PI) - ((angle (B,A,C)) / 3)) + (2 * PI)) - ((angle (B,A,C)) / 3) = (2 * PI) - (angle (B,A,C)) or (((2 * PI) - ((angle (B,A,C)) / 3)) + (2 * PI)) - ((angle (B,A,C)) / 3) = ((2 * PI) - (angle (B,A,C))) + (2 * PI) ) by A1, EUCLID10:31, A52, A53;

suppose A54: (((2 * PI) - ((angle (B,A,C)) / 3)) + (2 * PI)) - ((angle (B,A,C)) / 3) = (2 * PI) - (angle (B,A,C)) ; :: thesis: contradiction

0 < angle (B,A,C) by A16, Th4;
hence contradiction by A54, COMPTRIG:5; :: thesis: verum

end;

suppose (((2 * PI) - ((angle (B,A,C)) / 3)) + (2 * PI)) - ((angle (B,A,C)) / 3) = ((2 * PI) - (angle (B,A,C))) + (2 * PI) ; :: thesis: contradiction

hence contradiction by A16, Th4; :: thesis: verum

end;

end;

end;

end;

hence ( angle (F,A,E) <> PI & angle (A,E,F) <> PI & angle (E,F,A) <> PI ) ; :: thesis: verum

end;

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

end;

A55: - (the_diameter_of_the_circumcircle (C,B,A)) = the_diameter_of_the_circumcircle (A,B,C) by A1, EUCLID10:49;
set lambda = - ((((the_diameter_of_the_circumcircle (C,B,A)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3)));
A56: |.(A - E).| = - (((((the_diameter_of_the_circumcircle (C,B,A)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((angle (C,B,A)) / 3))) by A1, A2, A3, A4, A15, A20, A10, EUCLID10:56
.= (- ((((the_diameter_of_the_circumcircle (C,B,A)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3)))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3))) ;
A57: |.(A - F).| = ((((the_diameter_of_the_circumcircle (A,B,C)) * 4) * (sin ((angle (C,B,A)) / 3))) * (sin ((PI / 3) + ((angle (C,B,A)) / 3)))) * (sin ((angle (A,C,B)) / 3)) by A1, A5, A6, A7, A11, A13, A22, Th8
.= (- ((((the_diameter_of_the_circumcircle (C,B,A)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3)))) * (sin ((PI / 3) + ((angle (C,B,A)) / 3))) by A55 ;
A58: C,A,B is_a_triangle by A1, MENELAUS:15;
then A59: (((PI / 3) + ((angle (A,C,B)) / 3)) + ((PI / 3) + ((angle (C,B,A)) / 3))) + (angle (E,A,F)) = PI by Th10, A5, A23, A18, A4, A7, A8;
A60: |.(F - E).| ^2 = ((|.(A - E).| ^2) + (|.(A - F).| ^2)) - (((2 * |.(A - E).|) * |.(A - F).|) * (cos (angle (E,A,F)))) by Th3
.= ((- ((((the_diameter_of_the_circumcircle (C,B,A)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3)))) ^2) * ((((sin ((PI / 3) + ((angle (A,C,B)) / 3))) ^2) + ((sin ((PI / 3) + ((angle (C,B,A)) / 3))) ^2)) - (((2 * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((PI / 3) + ((angle (C,B,A)) / 3)))) * (cos (angle (E,A,F))))) by A56, A57
.= ((- ((((the_diameter_of_the_circumcircle (C,B,A)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3)))) ^2) * ((sin (angle (E,A,F))) ^2) by A59, EUCLID10:25
.= ((- ((((the_diameter_of_the_circumcircle (C,B,A)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3)))) ^2) * ((sin ((angle (B,A,C)) / 3)) ^2) by Th9, A58, A5, A23, A18, A4, A7
.= ((- ((((the_diameter_of_the_circumcircle (C,B,A)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3)))) * (sin ((angle (B,A,C)) / 3))) ^2 ;

now :: thesis: ( 0 <= - ((((the_diameter_of_the_circumcircle (C,B,A)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3))) & 0 <= sin ((angle (B,A,C)) / 3) )

A61: - ((((the_diameter_of_the_circumcircle (C,B,A)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3))) = (((- (the_diameter_of_the_circumcircle (C,B,A))) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3))
.= (((the_diameter_of_the_circumcircle (A,B,C)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3)) by A1, EUCLID10:49 ;

now :: thesis: ( sin ((angle (C,B,A)) / 3) >= 0 & 0 <= sin ((angle (A,C,B)) / 3) & 0 <= the_diameter_of_the_circumcircle (A,B,C) )

( 0 <= angle (C,B,A) & angle (C,B,A) < PI ) by A14, A12, A8, Th4;
then A62: ( 0 <= (angle (C,B,A)) / 3 & (angle (C,B,A)) / 3 < PI / 3 ) by XREAL_1:74;
PI / 3 < PI / 1 by COMPTRIG:5, XREAL_1:76;
then ( (2 * PI) * 0 <= (angle (C,B,A)) / 3 & (angle (C,B,A)) / 3 < PI + ((2 * PI) * 0) ) by A62, XXREAL_0:2;
hence sin ((angle (C,B,A)) / 3) >= 0 by SIN_COS6:16; :: thesis: ( 0 <= sin ((angle (A,C,B)) / 3) & 0 <= the_diameter_of_the_circumcircle (A,B,C) )
( 0 <= angle (A,C,B) & angle (A,C,B) < PI ) by A8, Th2;
then A63: ( 0 <= (angle (A,C,B)) / 3 & (angle (A,C,B)) / 3 < PI / 3 ) by XREAL_1:74;
PI / 3 < PI / 1 by COMPTRIG:5, XREAL_1:76;
then ( (2 * PI) * 0 <= (angle (A,C,B)) / 3 & (angle (A,C,B)) / 3 < PI + ((2 * PI) * 0) ) by A63, XXREAL_0:2;
hence 0 <= sin ((angle (A,C,B)) / 3) by SIN_COS6:16; :: thesis: 0 <= the_diameter_of_the_circumcircle (A,B,C)
thus 0 <= the_diameter_of_the_circumcircle (A,B,C) by A15, Th6; :: thesis: verum

end;

hence 0 <= - ((((the_diameter_of_the_circumcircle (C,B,A)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3))) by A61; :: thesis: 0 <= sin ((angle (B,A,C)) / 3)

now :: thesis: ( A,C,B are_mutually_distinct & 0 < angle (A,C,B) & angle (A,C,B) < PI )

A,C,B is_a_triangle by A1, MENELAUS:15;
hence A,C,B are_mutually_distinct by EUCLID_6:20; :: thesis: ( 0 < angle (A,C,B) & angle (A,C,B) < PI )
angle (A,C,B) <> 0 by A1, EUCLID10:30;
hence ( 0 < angle (A,C,B) & angle (A,C,B) < PI ) by A8, Th2; :: thesis: verum

end;

then ( 0 <= angle (B,A,C) & angle (B,A,C) < PI ) by Th4;
then A64: ( 0 <= (angle (B,A,C)) / 3 & (angle (B,A,C)) / 3 < PI / 3 ) by XREAL_1:74;
PI / 3 < PI / 1 by COMPTRIG:5, XREAL_1:76;
then ( (2 * PI) * 0 <= (angle (B,A,C)) / 3 & (angle (B,A,C)) / 3 < PI + ((2 * PI) * 0) ) by A64, XXREAL_0:2;
hence 0 <= sin ((angle (B,A,C)) / 3) by SIN_COS6:16; :: thesis: verum

end;

then A65: sqrt (((- ((((the_diameter_of_the_circumcircle (C,B,A)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3)))) * (sin ((angle (B,A,C)) / 3))) ^2) = (- ((((the_diameter_of_the_circumcircle (C,B,A)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3)))) * (sin ((angle (B,A,C)) / 3)) by SQUARE_1:22;
- ((((the_diameter_of_the_circumcircle (C,B,A)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3))) = (((- (the_diameter_of_the_circumcircle (C,B,A))) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3))
.= (((the_diameter_of_the_circumcircle (A,B,C)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3)) by A1, EUCLID10:49 ;
hence |.(F - E).| = (((4 * (the_diameter_of_the_circumcircle (A,B,C))) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3))) * (sin ((angle (B,A,C)) / 3)) by A60, SQUARE_1:22, A65; :: thesis: verum