euclid11.miz



    begin

    reserve A,B,C,D,E,F,G for Point of ( TOP-REAL 2);

    theorem :: EUCLID11:1

    

     Th1: ( angle (A,B,A)) = 0

    proof

       0 = ( angle (( euc2cpx A),( euc2cpx B),( euc2cpx A))) by COMPLEX2: 79

      .= ( angle (A,B,A)) by EUCLID_3:def 4;

      hence thesis;

    end;

    theorem :: EUCLID11:2

    

     Th2: 0 <= ( angle (A,B,C)) < (2 * PI )

    proof

      ( angle (A,B,C)) = ( angle (( euc2cpx A),( euc2cpx B),( euc2cpx C))) by EUCLID_3:def 4;

      hence thesis by COMPLEX2: 70;

    end;

    

     Lm1: [. 0 , (2 * PI ).[ = (( [. 0 , PI .[ \/ { PI }) \/ ]. PI , (2 * PI ).[)

    proof

       [. 0 , (2 * PI ).[ = ( [. 0 , PI .] \/ ]. PI , (2 * PI ).[) by COMPTRIG: 5, XXREAL_1: 169

      .= (( [. 0 , PI .[ \/ { PI }) \/ ]. PI , (2 * PI ).[) by COMPTRIG: 5, XXREAL_1: 129;

      hence thesis;

    end;

    theorem :: EUCLID11:3

     0 <= ( angle (A,B,C)) < PI or ( angle (A,B,C)) = PI or PI < ( angle (A,B,C)) < (2 * PI )

    proof

      set alpha = ( angle (A,B,C));

       0 <= alpha < (2 * PI ) by Th2;

      then alpha in (( [. 0 , PI .[ \/ { PI }) \/ ]. PI , (2 * PI ).[) by Lm1, XXREAL_1: 3;

      then alpha in ( [. 0 , PI .[ \/ { PI }) or alpha in ]. PI , (2 * PI ).[ by XBOOLE_0:def 3;

      then alpha in [. 0 , PI .[ or alpha in { PI } or alpha in ]. PI , (2 * PI ).[ by XBOOLE_0:def 3;

      hence thesis by XXREAL_1: 3, TARSKI:def 1, XXREAL_1: 4;

    end;

    theorem :: EUCLID11:4

    

     Th3: ( |.(F - E).| ^2 ) = ((( |.(A - E).| ^2 ) + ( |.(A - F).| ^2 )) - (((2 * |.(A - E).|) * |.(A - F).|) * ( cos ( angle (E,A,F)))))

    proof

      ( |.(F - E).| ^2 ) = ((( |.(E - A).| ^2 ) + ( |.(F - A).| ^2 )) - (((2 * |.(E - A).|) * |.(F - A).|) * ( cos ( angle (E,A,F))))) by EUCLID_6: 7

      .= ((( |.(A - E).| ^2 ) + ( |.(F - A).| ^2 )) - (((2 * |.(E - A).|) * |.(F - A).|) * ( cos ( angle (E,A,F))))) by EUCLID_6: 43

      .= ((( |.(A - E).| ^2 ) + ( |.(A - F).| ^2 )) - (((2 * |.(E - A).|) * |.(F - A).|) * ( cos ( angle (E,A,F))))) by EUCLID_6: 43

      .= ((( |.(A - E).| ^2 ) + ( |.(A - F).| ^2 )) - (((2 * |.(A - E).|) * |.(F - A).|) * ( cos ( angle (E,A,F))))) by EUCLID_6: 43

      .= ((( |.(A - E).| ^2 ) + ( |.(A - F).| ^2 )) - (((2 * |.(A - E).|) * |.(A - F).|) * ( cos ( angle (E,A,F))))) by EUCLID_6: 43;

      hence thesis;

    end;

    

     Lm2: for i be Integer st i > 0 holds ex k be Nat st i = k

    proof

      let i be Integer;

      assume

       A1: i > 0 ;

      i in INT by INT_1:def 2;

      then

      consider k be Nat such that

       A2: i = k or i = ( - k) by INT_1:def 1;

       0 <= k by NAT_1: 2;

      hence thesis by A1, A2;

    end;

    

     Lm3: for i be Integer st i < 0 holds ex k be Nat st i = ( - k)

    proof

      let i be Integer;

      assume

       A1: i < 0 ;

      i in INT by INT_1:def 2;

      then

      consider k be Nat such that

       A2: i = k or i = ( - k) by INT_1:def 1;

      thus thesis by A1, A2, NAT_1: 2;

    end;

    

     Lm4: for i be Integer st (3 * i) <= 1 & 0 < (1 + (3 * i)) holds i = 0

    proof

      let i be Integer;

      assume that

       A1: (3 * i) <= 1 and

       A2: 0 < (1 + (3 * i));

      assume

       A3: not i = 0 ;

      per cases ;

        suppose i < 0 ;

        then

        consider k be Nat such that

         A4: i = ( - k) by Lm3;

        ( 0 + (3 * k)) < ((1 - (3 * k)) + (3 * k)) by A2, A4, XREAL_1: 8;

        then

         A5: ((3 * k) / 3) < (1 / 3) by XREAL_1: 74;

        k <> 0 by A3, A4;

        then

        consider j be Nat such that

         A6: k = (j + 1) by NAT_1: 6;

        ((j + 1) - 1) < ((1 / 3) - 1) by A6, A5, XREAL_1: 8;

        then (j + 0 ) < ( - (2 / 3));

        hence contradiction by NAT_1: 2;

      end;

        suppose

         A7: i > 0 ;

        then

        consider k be Nat such that

         A8: i = k by Lm2;

        consider j be Nat such that

         A9: k = (j + 1) by A7, A8, NAT_1: 6;

        ((k * 3) / 3) <= (1 / 3) by A1, A8, XREAL_1: 72;

        then ((j + 1) - 1) <= ((1 / 3) - 1) by A9, XREAL_1: 9;

        then (j + 0 ) <= ( - (2 / 3));

        hence contradiction by NAT_1: 2;

      end;

    end;

    theorem :: EUCLID11:5

    

     Th4: (A,B,C) are_mutually_distinct & 0 < ( angle (A,B,C)) < PI implies 0 < ( angle (B,C,A)) < PI & 0 < ( angle (C,A,B)) < PI

    proof

      assume that

       A1: (A,B,C) are_mutually_distinct and

       A2: 0 < ( angle (A,B,C)) < PI ;

      set z1 = ( euc2cpx A);

      set z2 = ( euc2cpx B);

      set z3 = ( euc2cpx C);

      z1 <> z2 & z2 <> z3 & z1 <> z3 & 0 < ( angle (z1,z2,z3)) < PI by A1, A2, EUCLID_3: 4, EUCLID_3:def 4;

      then

       A3: 0 < ( angle (z2,z3,z1)) & 0 < ( angle (z3,z1,z2)) by COMPLEX2: 84;

      then

       A4: 0 < ( angle (B,C,A)) & 0 < ( angle (C,A,B)) by EUCLID_3:def 4;

      

       A5: ((( angle (A,B,C)) + ( angle (B,C,A))) + ( angle (C,A,B))) = PI by A1, A2, EUCLID_3: 47;

      now

        assume PI <= ( angle (B,C,A)) or PI <= ( angle (C,A,B));

        per cases ;

          suppose PI <= ( angle (B,C,A));

          then (( angle (A,B,C)) + PI ) <= (( angle (A,B,C)) + ( angle (B,C,A))) by XREAL_1: 6;

          then

           A6: ((( angle (A,B,C)) + PI ) + ( angle (C,A,B))) <= PI by A5, XREAL_1: 6;

          ( 0 + PI ) < (( angle (A,B,C)) + PI ) by A2, XREAL_1: 6;

          hence contradiction by A4, XREAL_1: 8, A6;

        end;

          suppose PI <= ( angle (C,A,B));

          then (( angle (A,B,C)) + PI ) <= (( angle (A,B,C)) + ( angle (C,A,B))) by XREAL_1: 6;

          then

           A7: ((( angle (A,B,C)) + PI ) + ( angle (B,C,A))) <= ((( angle (A,B,C)) + ( angle (C,A,B))) + ( angle (B,C,A))) by XREAL_1: 6;

          ( 0 + PI ) < (( angle (A,B,C)) + PI ) by A2, XREAL_1: 6;

          hence contradiction by A7, A5, A4, XREAL_1: 8;

        end;

      end;

      hence thesis by A3, EUCLID_3:def 4;

    end;

    theorem :: EUCLID11:6

    (A,B,C) are_mutually_distinct & ( angle (A,B,C)) = 0 implies (( angle (B,C,A)) = 0 & ( angle (C,A,B)) = PI ) or (( angle (B,C,A)) = PI & ( angle (C,A,B)) = 0 ) & ((( angle (A,B,C)) + ( angle (B,C,A))) + ( angle (C,A,B))) = PI

    proof

      assume that

       A1: (A,B,C) are_mutually_distinct and

       A2: ( angle (A,B,C)) = 0 ;

      set z1 = ( euc2cpx A);

      set z2 = ( euc2cpx B);

      set z3 = ( euc2cpx C);

      z1 <> z2 & z2 <> z3 & z1 <> z3 & ( angle (z1,z2,z3)) = 0 by A1, A2, EUCLID_3: 4, EUCLID_3:def 4;

      per cases by COMPLEX2: 87;

        suppose ( angle (z2,z3,z1)) = 0 & ( angle (z3,z1,z2)) = PI ;

        hence thesis by EUCLID_3:def 4;

      end;

        suppose ( angle (z2,z3,z1)) = PI & ( angle (z3,z1,z2)) = 0 ;

        then ( angle (B,C,A)) = PI & ( angle (C,A,B)) = 0 by EUCLID_3:def 4;

        hence thesis by A2;

      end;

    end;

    theorem :: EUCLID11:7

    (A,B,C) are_mutually_distinct & ( angle (A,B,C)) = PI implies ( angle (B,C,A)) = 0 & ( angle (C,A,B)) = 0 & ((( angle (A,B,C)) + ( angle (B,C,A))) + ( angle (C,A,B))) = PI

    proof

      assume that

       A1: (A,B,C) are_mutually_distinct and

       A2: ( angle (A,B,C)) = PI ;

      set z1 = ( euc2cpx A);

      set z2 = ( euc2cpx B);

      set z3 = ( euc2cpx C);

      z1 <> z2 & z2 <> z3 & z1 <> z3 & ( angle (z1,z2,z3)) = PI by A1, A2, EUCLID_3: 4, EUCLID_3:def 4;

      then ( angle (z2,z3,z1)) = 0 & ( angle (z3,z1,z2)) = 0 by COMPLEX2: 86;

      hence ( angle (B,C,A)) = 0 & ( angle (C,A,B)) = 0 by EUCLID_3:def 4;

      hence thesis by A2;

    end;

    theorem :: EUCLID11:8

    (A,B,C) are_mutually_distinct & ( angle (A,B,C)) > PI implies ( angle (B,C,A)) > PI & ( angle (C,A,B)) > PI

    proof

      assume

       A1: (A,B,C) are_mutually_distinct & ( angle (A,B,C)) > PI ;

      set z1 = ( euc2cpx A);

      set z2 = ( euc2cpx B);

      set z3 = ( euc2cpx C);

      z1 <> z2 & z2 <> z3 & z1 <> z3 & ( angle (z1,z2,z3)) > PI by A1, EUCLID_3: 4, EUCLID_3:def 4;

      then ( angle (z2,z3,z1)) > PI & ( angle (z3,z1,z2)) > PI by COMPLEX2: 85;

      hence thesis by EUCLID_3:def 4;

    end;

    theorem :: EUCLID11:9

    (A,B,C) are_mutually_distinct & ( angle (A,B,C)) > PI implies ((( angle (A,B,C)) + ( angle (B,C,A))) + ( angle (C,A,B))) = (5 * PI )

    proof

      assume that

       A1: (A,B,C) are_mutually_distinct and

       A2: ( angle (A,B,C)) > PI ;

      ( angle (A,B,C)) <> 0 & ( angle (B,C,A)) <> 0 & ( angle (C,A,B)) <> 0 by A1, A2, COMPTRIG: 5, EUCLID_6: 24;

      then

       A3: ( angle (A,B,C)) = ((2 * PI ) - ( angle (C,B,A))) & ( angle (B,C,A)) = ((2 * PI ) - ( angle (A,C,B))) & ( angle (C,A,B)) = ((2 * PI ) - ( angle (B,A,C))) by EUCLID_3: 38;

      ((2 * PI ) - ( angle (A,B,C))) < ((2 * PI ) - PI ) by A2, XREAL_1: 15;

      then ((( angle (C,B,A)) + ( angle (B,A,C))) + ( angle (A,C,B))) = PI by A1, A3, EUCLID_3: 47;

      hence thesis by A3;

    end;

    

     Lm5: for a be Real holds ( sin (((4 * PI ) / 3) - a)) = ( - ( sin (( PI / 3) - a)))

    proof

      let a be Real;

      ( sin (((4 * PI ) / 3) - a)) = ( sin ( PI + (( PI / 3) - a)))

      .= ( - ( sin (( PI / 3) - a))) by SIN_COS: 79;

      hence thesis;

    end;

    theorem :: EUCLID11:10

    

     Th5: ( angle (C,B,A)) < PI implies 0 <= ( the_area_of_polygon3 (A,B,C))

    proof

      assume ( angle (C,B,A)) < PI ;

      then ((2 * PI ) * 0 ) <= ( angle (C,B,A)) < ( PI + ((2 * PI ) * 0 )) by Th2;

      then

       A1: ( sin ( angle (C,B,A))) >= 0 by SIN_COS6: 16;

      ( the_area_of_polygon3 (A,B,C)) = ((( |.(A - B).| * |.(C - B).|) * ( sin ( angle (C,B,A)))) / 2) by EUCLID_6: 5;

      hence thesis by A1;

    end;

    theorem :: EUCLID11:11

    

     Th6: ( angle (C,B,A)) < PI implies 0 <= ( the_diameter_of_the_circumcircle (A,B,C))

    proof

      assume ( angle (C,B,A)) < PI ;

      then 0 <= ( the_area_of_polygon3 (A,B,C)) by Th5;

      hence thesis;

    end;

    begin

    theorem :: EUCLID11:12

    

     Th7: (A,F,C) is_a_triangle & ( angle (C,F,A)) < PI & ( angle (A,C,F)) = (( angle (A,C,B)) / 3) & ( angle (F,A,C)) = (( angle (B,A,C)) / 3) & (((( angle (A,C,B)) / 3) + (( angle (B,A,C)) / 3)) + (( angle (C,B,A)) / 3)) = ( PI / 3) implies ( |.(A - F).| * ( sin (( PI / 3) - (( angle (C,B,A)) / 3)))) = ( |.(A - C).| * ( sin (( angle (A,C,B)) / 3)))

    proof

      assume that

       A1: (A,F,C) is_a_triangle and

       A2: ( angle (C,F,A)) < PI and

       A3: ( angle (A,C,F)) = (( angle (A,C,B)) / 3) and

       A4: ( angle (F,A,C)) = (( angle (B,A,C)) / 3) and

       A5: (((( angle (A,C,B)) / 3) + (( angle (B,A,C)) / 3)) + (( angle (C,B,A)) / 3)) = ( PI / 3);

      

       A6: ( angle (F,C,A)) = ((2 * PI ) - (( angle (A,C,B)) / 3)) by A1, A3, EUCLID10: 31;

      

       A7: ( angle (A,C,F)) = ((2 * PI ) - ( angle (F,C,A))) & ( angle (F,A,C)) = ((2 * PI ) - ( angle (C,A,F))) by A1, EUCLID10: 31;

      

       A8: (A,F,C) are_mutually_distinct by A1, EUCLID_6: 20;

      (F,A,C) is_a_triangle & ( angle (C,F,A)) < PI by A1, A2, MENELAUS: 15;

      then ((( angle (C,A,F)) + ( angle (A,F,C))) + ( angle (F,C,A))) = (5 * PI ) by EUCLID10: 54;

      then ( angle (A,F,C)) = (((4 * PI ) / 3) - (( angle (C,B,A)) / 3)) by A7, A3, A5, A4;

      then

       A9: ( sin ( angle (A,F,C))) = ( - ( sin (( PI / 3) - (( angle (C,B,A)) / 3)))) by Lm5;

      ( |.(A - F).| * ( sin ( angle (A,F,C)))) = ( |.(A - C).| * ( sin ((2 * PI ) - (( angle (A,C,B)) / 3)))) by A8, A6, EUCLID_6: 6;

      then ( |.(A - F).| * ( - ( sin (( PI / 3) - (( angle (C,B,A)) / 3))))) = ( |.(A - C).| * ( - ( sin (( angle (A,C,B)) / 3)))) by A9, EUCLID10: 3;

      hence thesis;

    end;

    theorem :: EUCLID11:13

    

     Th8: (A,B,C) is_a_triangle & (A,F,C) is_a_triangle & ( angle (C,F,A)) < PI & ( angle (A,C,F)) = (( angle (A,C,B)) / 3) & ( angle (F,A,C)) = (( angle (B,A,C)) / 3) & (((( angle (A,C,B)) / 3) + (( angle (B,A,C)) / 3)) + (( angle (C,B,A)) / 3)) = ( PI / 3) & ( sin (( PI / 3) - (( angle (C,B,A)) / 3))) <> 0 implies |.(A - F).| = ((((4 * ( the_diameter_of_the_circumcircle (A,B,C))) * ( sin (( angle (C,B,A)) / 3))) * ( sin (( PI / 3) + (( angle (C,B,A)) / 3)))) * ( sin (( angle (A,C,B)) / 3)))

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: (A,F,C) is_a_triangle and

       A3: ( angle (C,F,A)) < PI and

       A4: ( angle (A,C,F)) = (( angle (A,C,B)) / 3) and

       A5: ( angle (F,A,C)) = (( angle (B,A,C)) / 3) and

       A6: (((( angle (A,C,B)) / 3) + (( angle (B,A,C)) / 3)) + (( angle (C,B,A)) / 3)) = ( PI / 3) and

       A7: ( sin (( PI / 3) - (( angle (C,B,A)) / 3))) <> 0 ;

      

       A8: ( |.(A - F).| * ( sin (( PI / 3) - (( angle (C,B,A)) / 3)))) = ( |.(A - C).| * ( sin (( angle (A,C,B)) / 3))) by A3, A4, A5, A2, A6, Th7

      .= ( |.(C - A).| * ( sin (( angle (A,C,B)) / 3))) by EUCLID_6: 43

      .= ((( the_diameter_of_the_circumcircle (A,B,C)) * ( sin ( angle (C,B,A)))) * ( sin (( angle (A,C,B)) / 3))) by A1, EUCLID10: 50;

      ( sin ( angle (C,B,A))) = ( sin (3 * (( angle (C,B,A)) / 3)))

      .= (((4 * ( sin (( angle (C,B,A)) / 3))) * ( sin (( PI / 3) + (( angle (C,B,A)) / 3)))) * ( sin (( PI / 3) - (( angle (C,B,A)) / 3)))) by EUCLID10: 29;

      then |.(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))) * ( sin (( PI / 3) - (( angle (C,B,A)) / 3)))) / ( sin (( PI / 3) - (( angle (C,B,A)) / 3)))) by A7, A8, XCMPLX_1: 89;

      then

       A9: |.(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))) * (( sin (( PI / 3) - (( angle (C,B,A)) / 3))) / ( sin (( PI / 3) - (( angle (C,B,A)) / 3)))));

      (( sin (( PI / 3) - (( angle (C,B,A)) / 3))) / ( sin (( PI / 3) - (( angle (C,B,A)) / 3)))) = 1 by A7, XCMPLX_1: 60;

      hence thesis by A9;

    end;

    theorem :: EUCLID11:14

    

     Th9: (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)

    proof

      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);

      

       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));

        now

          ( 0 + (2 * PI )) < ((2 * PI ) + (2 * PI )) by COMPTRIG: 5, XREAL_1: 8;

          hence (2 * PI ) < (4 * PI );

           0 <= ( angle (B,A,C)) & ( angle (B,A,C)) <> 0 by Th2, A1, EUCLID10: 30;

          hence 0 < (( angle (B,A,C)) / 3);

        end;

        then ((2 * PI ) + 0 ) < ((4 * PI ) + (( angle (B,A,C)) / 3)) by XREAL_1: 8;

        hence contradiction by A14, Th2;

      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));

         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;

      end;

      hence thesis by A12, A7, A8, A9, A10, A11, A13;

    end;

    theorem :: EUCLID11:15

    

     Th10: (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

    proof

      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);

      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 thesis by A8;

    end;

    theorem :: EUCLID11:16

    

     Th11: (A,C,B) is_a_triangle implies ( sin (( PI / 3) - (( angle (A,C,B)) / 3))) <> 0

    proof

      assume

       A1: (A,C,B) is_a_triangle ;

      assume ( sin (( PI / 3) - (( angle (A,C,B)) / 3))) = 0 ;

      then

      consider i0 be Integer such that

       A2: (( PI / 3) - (( angle (A,C,B)) / 3)) = ( PI * i0) by BORSUK_7: 7;

      ( 0 + ((3 * i0) * PI )) <= (( PI - ((3 * i0) * PI )) + ((3 * i0) * PI )) & (( PI - ((3 * i0) * PI )) + ((3 * i0) * PI )) < ((2 * PI ) + ((3 * i0) * PI )) by A2, XREAL_1: 6, Th2;

      then ((3 * i0) * PI ) <= PI & ( PI - PI ) < (((2 * PI ) + ((3 * i0) * PI )) - PI ) by XREAL_1: 9;

      then (((3 * i0) * PI ) / PI ) <= ( PI / PI ) & 0 < ((1 + (3 * i0)) * PI ) by COMPTRIG: 5, XREAL_1: 72;

      then ((3 * i0) * ( PI / PI )) <= ( PI / PI ) & ( 0 / PI ) < (((1 + (3 * i0)) * PI ) / PI ) by COMPTRIG: 5;

      then (3 * i0) <= ( PI / PI ) & ( 0 / PI ) < (1 + (3 * i0)) by XCMPLX_1: 88, COMPTRIG: 5;

      then (3 * i0) <= 1 & 0 < (1 + (3 * i0)) by XCMPLX_1: 60;

      then i0 = 0 by Lm4;

      hence contradiction by A1, A2, EUCLID_6: 20;

    end;

    theorem :: EUCLID11:17

    

     Th12: (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)))

    proof

      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 ;

      

       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)) < 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)) < 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)) < 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

          E <> F

          proof

            assume

             A24: E = F;

            per cases by EUCLID_6: 4;

              suppose

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

              

               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;

            end;

              suppose

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

              

               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;

            end;

          end;

          hence (F,A,E) are_mutually_distinct by A21, A19;

          now

            hereby

              assume

               A30: ( angle (F,A,E)) = PI ;

              

               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 by EUCLID_6: 4;

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

                per cases by A31, A30;

                  suppose

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

                  

                   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,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;

                end;

                  suppose

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

                  

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

                end;

              end;

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

                per cases by A31, A30;

                  suppose

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

                  

                   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;

                end;

                  suppose

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

                  

                   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;

                end;

              end;

            end;

            hereby

              assume ( angle (A,E,F)) = PI ;

              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 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)));

                 0 < ( angle (B,A,C)) by A16, Th4;

                hence contradiction by A50, COMPTRIG: 5;

              end;

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

                hence contradiction by A16, Th4;

              end;

            end;

            hereby

              assume ( angle (E,F,A)) = PI ;

              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 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)));

                 0 < ( angle (B,A,C)) by A16, Th4;

                hence contradiction by A54, COMPTRIG: 5;

              end;

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

                hence contradiction by A16, Th4;

              end;

            end;

          end;

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

        end;

        hence thesis by EUCLID_6: 20;

      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

      .= (lambda * ( 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

      .= (lambda * ( 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

      .= ((lambda ^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

      .= ((lambda ^2 ) * (( sin ( angle (E,A,F))) ^2 )) by A59, EUCLID10: 25

      .= ((lambda ^2 ) * (( sin (( angle (B,A,C)) / 3)) ^2 )) by Th9, A58, A5, A23, A18, A4, A7

      .= ((lambda * ( sin (( angle (B,A,C)) / 3))) ^2 );

      now

        

         A61: lambda = (((( - ( 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

           0 <= ( angle (C,B,A)) < PI by A14, A12, A8, Th4;

          then

           A62: 0 <= (( 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) < ( PI + ((2 * PI ) * 0 )) by A62, XXREAL_0: 2;

          hence ( sin (( angle (C,B,A)) / 3)) >= 0 by SIN_COS6: 16;

           0 <= ( angle (A,C,B)) < PI by A8, Th2;

          then

           A63: 0 <= (( 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) < ( PI + ((2 * PI ) * 0 )) by A63, XXREAL_0: 2;

          hence 0 <= ( sin (( angle (A,C,B)) / 3)) by SIN_COS6: 16;

          thus 0 <= ( the_diameter_of_the_circumcircle (A,B,C)) by A15, Th6;

        end;

        hence 0 <= lambda by A61;

        now

          (A,C,B) is_a_triangle by A1, MENELAUS: 15;

          hence (A,C,B) are_mutually_distinct by EUCLID_6: 20;

          ( angle (A,C,B)) <> 0 by A1, EUCLID10: 30;

          hence 0 < ( angle (A,C,B)) < PI by A8, Th2;

        end;

        then 0 <= ( angle (B,A,C)) < PI by Th4;

        then

         A64: 0 <= (( 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) < ( PI + ((2 * PI ) * 0 )) by A64, XXREAL_0: 2;

        hence 0 <= ( sin (( angle (B,A,C)) / 3)) by SIN_COS6: 16;

      end;

      then

       A65: ( sqrt ((lambda * ( sin (( angle (B,A,C)) / 3))) ^2 )) = (lambda * ( sin (( angle (B,A,C)) / 3))) by SQUARE_1: 22;

      lambda = (((( - ( 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 thesis by A60, SQUARE_1: 22, A65;

    end;

    theorem :: EUCLID11:18

    

     Th13: (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

    proof

      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);

      

       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

        thus (A,B,E) are_mutually_distinct by A4, A2, Th1, A3, A5;

        hereby

          assume ( angle (A,B,E)) = PI ;

          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;

        end;

        hereby

          assume ( angle (B,E,A)) = PI ;

          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;

        end;

        hereby

          assume

           A6: ( angle (E,A,B)) = PI ;

          

          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;

        end;

      end;

      hence thesis by EUCLID_6: 20;

    end;

    theorem :: EUCLID11:19

    

     Th14: (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

    proof

      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);

      

       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

        thus (A,F,C) are_mutually_distinct by A2, A3, A4, A5, Th1;

        hereby

          assume ( angle (A,F,C)) = PI ;

          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;

        end;

        hereby

          assume

           A6: ( angle (C,A,F)) = PI ;

          

          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;

        end;

        hereby

          assume

           A8: ( angle (F,C,A)) = PI ;

          

          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;

        end;

      end;

      hence thesis by EUCLID_6: 20;

    end;

    theorem :: EUCLID11:20

    

     Th15: (A,B,C) is_a_triangle & ( angle (C,B,G)) = (( angle (C,B,A)) / 3) & ( angle (G,C,B)) = (( angle (A,C,B)) / 3) implies (C,G,B) is_a_triangle

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: ( angle (C,B,G)) = (( angle (C,B,A)) / 3) and

       A3: ( angle (G,C,B)) = (( angle (A,C,B)) / 3);

      

       A4: (A,B,C) are_mutually_distinct by A1, EUCLID_6: 20;

      

       A5: ( angle (A,C,B)) <> 0 & ( angle (C,B,A)) <> 0 by A1, EUCLID10: 30;

      now

        thus (C,G,B) are_mutually_distinct by A2, A3, A4, A5, Th1;

        hereby

          assume ( angle (C,G,B)) = PI ;

          then G in ( LSeg (C,B)) & G <> C by A2, A5, Th1, EUCLID_6: 11;

          

          then ( angle (G,C,B)) = ( angle (B,C,B)) by EUCLID_6: 9

          .= 0 by Th1;

          hence contradiction by A3, A1, EUCLID10: 30;

        end;

        hereby

          assume ( angle (G,B,C)) = PI ;

          

          then

           A6: ( angle (C,B,G)) = ((2 * PI ) - PI ) by COMPTRIG: 5, EUCLID_3: 37

          .= PI ;

          ((2 * PI ) + 0 ) < ((2 * PI ) + PI ) by COMPTRIG: 5, XREAL_1: 8;

          hence contradiction by A2, A6, Th2;

        end;

        hereby

          assume ( angle (B,C,G)) = PI ;

          

          then

           A7: ( angle (G,C,B)) = ((2 * PI ) - PI ) by COMPTRIG: 5, EUCLID_3: 37

          .= PI ;

          ((2 * PI ) + 0 ) < ((2 * PI ) + PI ) by COMPTRIG: 5, XREAL_1: 8;

          hence contradiction by A3, A7, Th2;

        end;

      end;

      hence thesis by EUCLID_6: 20;

    end;

    theorem :: EUCLID11:21

    

     Th16: (A,B,C) is_a_triangle & ( angle (A,C,B)) < PI & ( angle (E,B,A)) = (( angle (C,B,A)) / 3) & ( angle (B,A,E)) = (( angle (B,A,C)) / 3) & ( angle (A,C,F)) = (( angle (A,C,B)) / 3) & ( angle (F,A,C)) = (( angle (B,A,C)) / 3) & ( angle (C,B,G)) = (( angle (C,B,A)) / 3) & ( angle (G,C,B)) = (( angle (A,C,B)) / 3) 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))) & |.(G - F).| = ((((4 * ( the_diameter_of_the_circumcircle (C,A,B))) * ( sin (( angle (C,B,A)) / 3))) * ( sin (( angle (B,A,C)) / 3))) * ( sin (( angle (A,C,B)) / 3))) & |.(E - G).| = ((((4 * ( the_diameter_of_the_circumcircle (B,C,A))) * ( sin (( angle (B,A,C)) / 3))) * ( sin (( angle (A,C,B)) / 3))) * ( sin (( angle (C,B,A)) / 3)))

    proof

      assume

       A1: (A,B,C) is_a_triangle & ( angle (A,C,B)) < PI & ( angle (E,B,A)) = (( angle (C,B,A)) / 3) & ( angle (B,A,E)) = (( angle (B,A,C)) / 3) & ( angle (A,C,F)) = (( angle (A,C,B)) / 3) & ( angle (F,A,C)) = (( angle (B,A,C)) / 3) & ( angle (C,B,G)) = (( angle (C,B,A)) / 3) & ( angle (G,C,B)) = (( angle (A,C,B)) / 3);

      then

       A2: (A,B,E) is_a_triangle & (A,F,C) is_a_triangle & (C,G,B) is_a_triangle by Th13, Th14, Th15;

      now

        thus

         A3: (C,A,B) is_a_triangle & (B,C,A) is_a_triangle by A1, MENELAUS: 15;

        thus (C,A,F) is_a_triangle & (B,C,G) is_a_triangle & (B,E,A) is_a_triangle by A2, MENELAUS: 15;

        ( angle (A,C,B)) <> 0 by A1, EUCLID10: 30;

        then (A,C,B) are_mutually_distinct & 0 < ( angle (A,C,B)) < PI by A1, A3, EUCLID_6: 20, Th2;

        hence ( angle (C,B,A)) < PI & ( angle (B,A,C)) < PI by Th4;

      end;

      hence thesis by A1, A2, Th12;

    end;

    theorem :: EUCLID11:22

    

     Th17: (A,B,C) is_a_triangle & ( angle (A,C,B)) < PI & ( angle (E,B,A)) = (( angle (C,B,A)) / 3) & ( angle (B,A,E)) = (( angle (B,A,C)) / 3) & ( angle (A,C,F)) = (( angle (A,C,B)) / 3) & ( angle (F,A,C)) = (( angle (B,A,C)) / 3) & ( angle (C,B,G)) = (( angle (C,B,A)) / 3) & ( angle (G,C,B)) = (( angle (A,C,B)) / 3) implies |.(F - E).| = |.(G - F).| & |.(F - E).| = |.(E - G).| & |.(G - F).| = |.(E - G).|

    proof

      assume (A,B,C) is_a_triangle & ( angle (A,C,B)) < PI & ( angle (E,B,A)) = (( angle (C,B,A)) / 3) & ( angle (B,A,E)) = (( angle (B,A,C)) / 3) & ( angle (A,C,F)) = (( angle (A,C,B)) / 3) & ( angle (F,A,C)) = (( angle (B,A,C)) / 3) & ( angle (C,B,G)) = (( angle (C,B,A)) / 3) & ( angle (G,C,B)) = (( angle (A,C,B)) / 3);

      then

       A1: |.(F - E).| = ((((( the_diameter_of_the_circumcircle (A,B,C)) * 4) * ( sin (( angle (A,C,B)) / 3))) * ( sin (( angle (C,B,A)) / 3))) * ( sin (( angle (B,A,C)) / 3))) & |.(G - F).| = ((((( the_diameter_of_the_circumcircle (C,A,B)) * 4) * ( sin (( angle (C,B,A)) / 3))) * ( sin (( angle (B,A,C)) / 3))) * ( sin (( angle (A,C,B)) / 3))) & |.(E - G).| = ((((( the_diameter_of_the_circumcircle (B,C,A)) * 4) * ( sin (( angle (B,A,C)) / 3))) * ( sin (( angle (A,C,B)) / 3))) * ( sin (( angle (C,B,A)) / 3))) by Th16;

      ( the_diameter_of_the_circumcircle (A,B,C)) = ( the_diameter_of_the_circumcircle (C,A,B)) & ( the_diameter_of_the_circumcircle (A,B,C)) = ( the_diameter_of_the_circumcircle (B,C,A)) by EUCLID10: 46;

      hence thesis by A1;

    end;

    ::$Notion-Name

    theorem :: EUCLID11:23

    (A,B,C) is_a_triangle & ( angle (A,B,C)) < PI & ( angle (E,C,A)) = (( angle (B,C,A)) / 3) & ( angle (C,A,E)) = (( angle (C,A,B)) / 3) & ( angle (A,B,F)) = (( angle (A,B,C)) / 3) & ( angle (F,A,B)) = (( angle (C,A,B)) / 3) & ( angle (B,C,G)) = (( angle (B,C,A)) / 3) & ( angle (G,B,C)) = (( angle (A,B,C)) / 3) implies |.(F - E).| = |.(G - F).| & |.(F - E).| = |.(E - G).| & |.(G - F).| = |.(E - G).|

    proof

      assume

       A1: (A,B,C) is_a_triangle & ( angle (A,B,C)) < PI & ( angle (E,C,A)) = (( angle (B,C,A)) / 3) & ( angle (C,A,E)) = (( angle (C,A,B)) / 3) & ( angle (A,B,F)) = (( angle (A,B,C)) / 3) & ( angle (F,A,B)) = (( angle (C,A,B)) / 3) & ( angle (B,C,G)) = (( angle (B,C,A)) / 3) & ( angle (G,B,C)) = (( angle (A,B,C)) / 3);

      (A,C,B) is_a_triangle by A1, MENELAUS: 15;

      hence thesis by A1, Th17;

    end;