euclid13.miz



    begin

    reserve n for Nat;

    reserve i for Integer;

    reserve r,s,t for Real;

    reserve An,Bn,Cn,Dn for Point of ( TOP-REAL n);

    reserve L1,L2 for Element of ( line_of_REAL n);

    reserve A,B,C for Point of ( TOP-REAL 2);

    theorem :: EUCLID13:1

    

     Th1: 0 < (i * r) < r implies i = 1

    proof

      assume

       A1: 0 < (i * r) < r;

      assume not i = 1;

      then 0 < (1 - i) or 0 < (i - 1) by XREAL_1: 55;

      then ( 0 + i) < ((1 - i) + i) or ( 0 + 1) < ((i - 1) + 1) by XREAL_1: 8;

      per cases ;

        suppose i < 1;

        then i <= (1 - 1) by INT_1: 52;

        hence contradiction by A1;

      end;

        suppose i > 1;

        hence contradiction by A1, XREAL_1: 155;

      end;

    end;

    theorem :: EUCLID13:2

    

     Th2: for i be Integer st (( - 3) / 2) < i < (1 / 2) holds i = 0 or i = ( - 1)

    proof

      let i be Integer;

      assume

       A1: (( - 3) / 2) < i < (1 / 2);

      assume

       A2: not (i = 0 or i = ( - 1));

      ( - 2) < i < 1 by A1, XXREAL_0: 2;

      then

       A3: (( - 2) + 1) <= i & (i + 1) <= 1 & 0 <= 1 by INT_1: 7;

      then

       A4: ( - 1) <= i & ((i + 1) - 1) <= (1 - 1) by XREAL_1: 9;

      consider k be Nat such that

       A5: i = k or i = ( - k) by INT_1: 2;

      per cases by A5;

        suppose i = k;

        hence contradiction by A2, A4;

      end;

        suppose

         A6: i = ( - k);

        then (( - k) * ( - 1)) <= (( - 1) * ( - 1)) by A3, XREAL_1: 65;

        then k = 0 or ... or k = 1;

        hence contradiction by A6, A2;

      end;

    end;

    theorem :: EUCLID13:3

    

     Th3: r is non zero & s is non zero & t is non zero implies (((( - r) / ( - s)) * (( - t) / ( - r))) * (( - s) / ( - t))) = 1

    proof

      assume that

       A1: r is non zero and

       A2: s is non zero and

       A3: t is non zero;

      (((( - r) / ( - s)) * (( - t) / ( - r))) * (( - s) / ( - t))) = (((r / s) * (( - t) / ( - r))) * (( - s) / ( - t))) by XCMPLX_1: 191

      .= (((r / s) * (t / r)) * (( - s) / ( - t))) by XCMPLX_1: 191

      .= (((r / s) * (t / r)) * (s / t)) by XCMPLX_1: 191

      .= (((((r / r) * s) / s) * t) / t)

      .= ((((1 * s) / s) * t) / t) by A1, XCMPLX_1: 60

      .= (((1 * 1) * t) / t) by A2, XCMPLX_1: 60

      .= ((1 * 1) * 1) by A3, XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: EUCLID13:4

    

     Th4: 0 < r < (2 * PI ) implies ( sin (r / 2)) <> 0

    proof

      assume

       A1: 0 < r < (2 * PI );

      assume

       A2: ( sin (r / 2)) = 0 ;

      consider i0 be Integer such that

       A3: (r / 2) = ( PI * i0) by A2, BORSUK_7: 7;

      

       A4: r = ((2 * i0) * PI ) by A3;

      reconsider p = (2 * PI ) as Real;

       0 < (i0 * p) < p by A1, A4;

      then i0 = 1 by Th1;

      hence thesis by A1, A3;

    end;

    theorem :: EUCLID13:5

    

     Th5: ( - (2 * PI )) < r < 0 implies ( sin (r / 2)) <> 0

    proof

      assume

       A1: ( - (2 * PI )) < r < 0 ;

      assume

       A2: ( sin (r / 2)) = 0 ;

      ( 0 * ( - 1)) < (r * ( - 1)) & (r * ( - 1)) < (( - (2 * PI )) * ( - 1)) by A1, XREAL_1: 69;

      then

       A3: ( sin (( - r) / 2)) <> 0 by Th4;

      reconsider r0 = (r / 2) as Real;

      ( sin ( - r0)) = ( - ( sin r0)) by SIN_COS: 31;

      hence contradiction by A2, A3;

    end;

    theorem :: EUCLID13:6

    

     Th6: ( tan ((2 * PI ) - r)) = ( - ( tan r))

    proof

      ( tan ((2 * PI ) - r)) = (( - ( sin r)) / ( cos ((2 * PI ) - r))) by EUCLID10: 3

      .= ( - (( sin r) / ( cos ((2 * PI ) - r))))

      .= ( - ( tan r)) by EUCLID10: 4;

      hence thesis;

    end;

    theorem :: EUCLID13:7

    

     Th7: An in ( Line (Bn,Cn)) & An <> Cn implies ( Line (Bn,Cn)) = ( Line (An,Cn))

    proof

      assume that

       A1: An in ( Line (Bn,Cn)) and

       A2: An <> Cn;

      Cn in ( Line (Bn,Cn)) & An in ( Line (Bn,Cn)) by A1, EUCLID_4: 41;

      hence thesis by A2, EUCLID_4: 43, EUCLID_4: 42;

    end;

    theorem :: EUCLID13:8

    

     Th8: An <> Cn & An in ( Line (Bn,Cn)) implies Bn in ( Line (An,Cn))

    proof

      assume that

       A1: An <> Cn and

       A2: An in ( Line (Bn,Cn));

      Cn in ( Line (Bn,Cn)) by EUCLID_4: 41;

      then ( Line (Bn,Cn)) c= ( Line (An,Cn)) by A1, A2, EUCLID_4: 43;

      hence thesis by EUCLID_4: 41;

    end;

    theorem :: EUCLID13:9

    

     Th9: An <> Bn & An <> Cn & |((An - Bn), (An - Cn))| = 0 & L1 = ( Line (An,Bn)) & L2 = ( Line (An,Cn)) implies L1 _|_ L2

    proof

      assume that

       A1: An <> Bn and

       A2: An <> Cn and

       A3: |((An - Bn), (An - Cn))| = 0 and

       A4: L1 = ( Line (An,Bn)) and

       A5: L2 = ( Line (An,Cn));

      reconsider rA = An, rB = Bn, rC = Cn as Element of ( REAL n) by EUCLID: 22;

      

       A6: L1 = ( Line (rA,rB)) by A4, EUCLID12: 4;

      

       A7: L2 = ( Line (rA,rC)) by A5, EUCLID12: 4;

      

       A8: (rA - rB) <> ( 0* n) by A1, EUCLIDLP: 9;

      

       A9: (rA - rC) <> ( 0* n) by A2, EUCLIDLP: 9;

      (rA - rB) _|_ (rA - rC) by A8, A9, EUCLIDLP:def 3, A3, RVSUM_1:def 17;

      hence thesis by A6, A7, EUCLIDLP:def 8;

    end;

    theorem :: EUCLID13:10

    Bn <> Cn & |((Bn - An), (Bn - Cn))| = 0 implies An <> Cn

    proof

      assume that

       A1: Bn <> Cn and

       A2: |((Bn - An), (Bn - Cn))| = 0 ;

      assume

       A3: An = Cn;

      reconsider rB = Bn, rC = Cn as Element of ( REAL n) by EUCLID: 22;

      (rB - rC) = ( 0* n) by A2, A3, EUCLID_4: 17;

      hence contradiction by A1, EUCLIDLP: 9;

    end;

    theorem :: EUCLID13:11

    

     Th10: |((An - Bn), (An - Cn))| = |((Bn - An), (Cn - An))|

    proof

      

       A1: |((An - Bn), (An - Cn))| = |(( - (An - Bn)), ( - (An - Cn)))| by EUCLID_2: 23;

      ( - (An - Bn)) = (Bn - An) & ( - (Cn - An)) = (An - Cn) by RVSUM_1: 35;

      hence thesis by A1;

    end;

    theorem :: EUCLID13:12

    

     Th11: Bn <> Cn & r = ( - (((( |(Bn, Cn)| - |(Cn, Cn)|) - |(An, Bn)|) + |(An, Cn)|) / |((Bn - Cn), (Bn - Cn))|)) & Dn = ((r * Bn) + ((1 - r) * Cn)) implies |((Dn - An), (Dn - Cn))| = 0

    proof

      assume that

       A1: Bn <> Cn and

       A2: r = ( - (((( |(Bn, Cn)| - |(Cn, Cn)|) - |(An, Bn)|) + |(An, Cn)|) / |((Bn - Cn), (Bn - Cn))|)) and

       A3: Dn = ((r * Bn) + ((1 - r) * Cn));

      reconsider rA = An, rB = Bn, rC = Cn, rD = Dn as Element of ( REAL n) by EUCLID: 22;

      reconsider rrB = (r * rB), rrC = ((1 - r) * rC) as Element of ( REAL n);

      

       A4: |(rrB, rrB)| = (r * |(rB, rrB)|) by EUCLID_4: 21

      .= (r * (r * |(rB, rB)|)) by EUCLID_4: 22

      .= ((r * r) * |(rB, rB)|);

      

       A5: |(rrB, rrC)| = (r * |(rB, rrC)|) by EUCLID_4: 21

      .= (r * ((1 - r) * |(rB, rC)|)) by EUCLID_4: 22

      .= ((r * (1 - r)) * |(rB, rC)|);

      

       A6: |(rrC, rrC)| = ((1 - r) * |(rC, rrC)|) by EUCLID_4: 21

      .= ((1 - r) * ((1 - r) * |(rC, rC)|)) by EUCLID_4: 22

      .= (((1 - r) * (1 - r)) * |(rC, rC)|);

      

       A7: |(rD, rD)| = (( |(rrB, rrB)| + (2 * |(rrB, rrC)|)) + |(rrC, rrC)|) by A3, RVSUM_1: 138

      .= ((((r * r) * |(rB, rB)|) + (((2 * r) * (1 - r)) * |(rB, rC)|)) + (((1 - r) * (1 - r)) * |(rC, rC)|)) by A4, A5, A6;

      

       A8: |(rD, rC)| = ( |(rrB, rC)| + |(rrC, rC)|) by A3, EUCLID_4: 20

      .= ((r * |(rB, rC)|) + |(rrC, rC)|) by EUCLID_4: 21

      .= ((r * |(rB, rC)|) + ((1 - r) * |(rC, rC)|)) by EUCLID_4: 21;

      

       A9: |(rA, rD)| = ( |(rA, rrB)| + |(rA, rrC)|) by A3, EUCLID_4: 28

      .= ((r * |(rA, rB)|) + |(rA, rrC)|) by EUCLID_4: 22

      .= ((r * |(rA, rB)|) + ((1 - r) * |(rA, rC)|)) by EUCLID_4: 22;

      

       A10: (( |(rB, rB)| - (2 * |(rB, rC)|)) + |(rC, rC)|) = |((rB - rC), (rB - rC))| by RVSUM_1: 139;

      

       A11: (rB - rC) <> ( 0* n) by A1, EUCLIDLP: 9;

      

       A12: (((((r * |((rB - rC), (rB - rC))|) + |(rB, rC)|) - |(rC, rC)|) - |(rA, rB)|) + |(rA, rC)|) = ((((( - ((((( |(rB, rC)| - |(rC, rC)|) - |(rA, rB)|) + |(rA, rC)|) / |((rB - rC), (rB - rC))|) * |((rB - rC), (rB - rC))|)) + |(rB, rC)|) - |(rC, rC)|) - |(rA, rB)|) + |(rA, rC)|) by A2

      .= ((((( - ((( |(rB, rC)| - |(rC, rC)|) - |(rA, rB)|) + |(rA, rC)|)) + |(rB, rC)|) - |(rC, rC)|) - |(rA, rB)|) + |(rA, rC)|) by A11, EUCLID_4: 17, XCMPLX_1: 87

      .= 0 ;

       |((rD - rA), (rD - rC))| = ((((((((r * r) * |(rB, rB)|) + ((2 * r) * |(rB, rC)|)) - (((2 * r) * r) * |(rB, rC)|)) + (( |(rC, rC)| - ((2 * r) * |(rC, rC)|)) + ((r * r) * |(rC, rC)|))) - ((r * |(rB, rC)|) + ((1 - r) * |(rC, rC)|))) - ((r * |(rA, rB)|) + ((1 - r) * |(rA, rC)|))) + |(rA, rC)|) by A9, A7, A8, RVSUM_1: 137

      .= (r * (((((((r * |(rB, rB)|) + |(rB, rC)|) - ((2 * r) * |(rB, rC)|)) + (r * |(rC, rC)|)) - |(rC, rC)|) - |(rA, rB)|) + |(rA, rC)|))

      .= 0 by A10, A12;

      hence thesis;

    end;

    theorem :: EUCLID13:13

    

     Th12: An <> Bn & Cn = ((r * An) + ((1 - r) * Bn)) & Cn = Bn implies r = 0

    proof

      assume that

       A1: An <> Bn and

       A2: Cn = ((r * An) + ((1 - r) * Bn)) and

       A3: Cn = Bn;

      reconsider rA = An, rB = Bn, rC = Cn as Element of ( REAL n) by EUCLID: 22;

      rC = ((r * rA) + ((1 * rB) - (r * rB))) by A2, EUCLIDLP: 11

      .= (((r * rA) + ( - (r * rB))) + (1 * rB)) by RVSUM_1: 15

      .= (((r * rA) - (r * rB)) + (1 * rB));

      

      then (( 0* n) + rB) = (((r * rA) - (r * rB)) + (1 * rB)) by A3, EUCLID_4: 1

      .= (((r * rA) - (r * rB)) + rB) by EUCLID_4: 3;

      then ( 0* n) = ((r * rA) - (r * rB)) by RVSUM_1: 25;

      then (r * (rA - rB)) = ( 0* n) by EUCLIDLP: 12;

      then r = 0 or (rA - rB) = ( 0* n) by EUCLID_4: 5;

      hence thesis by A1, EUCLIDLP: 9;

    end;

    theorem :: EUCLID13:14

    

     Th13: ((( |(Bn, Cn)| - |(Cn, Cn)|) - |(An, Bn)|) + |(An, Cn)|) = |((Cn - An), (Bn - Cn))| & ( |((Bn - Cn), (Bn - Cn))| + |((Cn - An), (Bn - Cn))|) = |((Bn - Cn), (Bn - An))|

    proof

      reconsider rA = An, rB = Bn, rC = Cn as Element of ( REAL n) by EUCLID: 22;

      ((rB - rC) + (rC - rA)) = (((rB - rC) + rC) - rA) by RVSUM_1: 40

      .= (rB - rA) by RVSUM_1: 43;

      hence thesis by EUCLID_4: 28, EUCLID_4: 31;

    end;

    theorem :: EUCLID13:15

    

     Th14: |((An - Bn), (An - Cn))| = ( - |((An - Bn), (Cn - An))|)

    proof

      reconsider rA = An, rB = Bn, rC = Cn as Element of ( REAL n) by EUCLID: 22;

       |((rA - rB), (rA - rC))| = |((rA - rB), ( - (rC - rA)))| by RVSUM_1: 35

      .= ( - |((rA - rB), (rC - rA))|) by EUCLID_4: 24;

      hence thesis;

    end;

    theorem :: EUCLID13:16

    

     Th15: |((Bn - An), (Cn - An))| = |((An - Bn), (An - Cn))|

    proof

      reconsider rA = An, rB = Bn, rC = Cn as Element of ( REAL n) by EUCLID: 22;

       |((rB - rA), (rC - rA))| = |(( - (rA - rB)), (rC - rA))| by RVSUM_1: 35

      .= |(( - (rA - rB)), ( - (rA - rC)))| by RVSUM_1: 35

      .= |((rA - rB), (rA - rC))| by EUCLID_4: 25;

      hence thesis;

    end;

    theorem :: EUCLID13:17

    

     Th16: |((Bn - An), (Cn - An))| = ( - |((Bn - An), (An - Cn))|)

    proof

       |((Bn - An), (Cn - An))| = |((An - Bn), (An - Cn))| by Th15;

      hence thesis by Th14;

    end;

    theorem :: EUCLID13:18

    

     Th17: Bn <> Cn & Cn <> An & An <> Bn & |((Cn - An), (Bn - Cn))| is non zero & |((Bn - Cn), (An - Bn))| is non zero & |((Cn - An), (An - Bn))| is non zero & r = ( - (((( |(Bn, Cn)| - |(Cn, Cn)|) - |(An, Bn)|) + |(An, Cn)|) / |((Bn - Cn), (Bn - Cn))|)) & s = ( - (((( |(Cn, An)| - |(An, An)|) - |(Bn, Cn)|) + |(Bn, An)|) / |((Cn - An), (Cn - An))|)) & t = ( - (((( |(An, Bn)| - |(Bn, Bn)|) - |(Cn, An)|) + |(Cn, Bn)|) / |((An - Bn), (An - Bn))|)) implies (((((r / (1 - r)) * s) / (1 - s)) * t) / (1 - t)) = 1

    proof

      assume that

       A1: Bn <> Cn and

       A2: Cn <> An and

       A3: An <> Bn and

       A4: |((Cn - An), (Bn - Cn))| is non zero & |((Bn - Cn), (An - Bn))| is non zero & |((Cn - An), (An - Bn))| is non zero and

       A5: r = ( - (((( |(Bn, Cn)| - |(Cn, Cn)|) - |(An, Bn)|) + |(An, Cn)|) / |((Bn - Cn), (Bn - Cn))|)) and

       A6: s = ( - (((( |(Cn, An)| - |(An, An)|) - |(Bn, Cn)|) + |(Bn, An)|) / |((Cn - An), (Cn - An))|)) and

       A7: t = ( - (((( |(An, Bn)| - |(Bn, Bn)|) - |(Cn, An)|) + |(Cn, Bn)|) / |((An - Bn), (An - Bn))|));

      reconsider rA = An, rB = Bn, rC = Cn as Element of ( REAL n) by EUCLID: 22;

      

       A8: (rB - rC) <> ( 0* n) by A1, EUCLIDLP: 9;

      

       A9: (rC - rA) <> ( 0* n) by A2, EUCLIDLP: 9;

      

       A10: (rA - rB) <> ( 0* n) by A3, EUCLIDLP: 9;

      set rBC = |((Bn - Cn), (Bn - Cn))|, rCA = |((Cn - An), (Cn - An))|, rAB = |((An - Bn), (An - Bn))|, A = An, B = Bn, C = Cn;

      

       A11: (r * rBC) = ( - ((((( |(B, C)| - |(C, C)|) - |(A, B)|) + |(A, C)|) / rBC) * rBC)) by A5

      .= ( - ((( |(B, C)| - |(C, C)|) - |(A, B)|) + |(A, C)|)) by A8, EUCLID_4: 17, XCMPLX_1: 87;

      (r / (1 - r)) = (((r / (1 - r)) * rBC) / rBC) by A8, EUCLID_4: 17, XCMPLX_1: 89

      .= (((r * rBC) / (1 - r)) / rBC)

      .= ((r * rBC) / ((1 - r) * rBC)) by XCMPLX_1: 78

      .= (( - ((( |(B, C)| - |(C, C)|) - |(A, B)|) + |(A, C)|)) / (((( |((B - C), (B - C))| + |(B, C)|) - |(C, C)|) - |(A, B)|) + |(A, C)|)) by A11;

      

      then

       A12: (r / (1 - r)) = (( - |((C - A), (B - C))|) / ( |((B - C), (B - C))| + ((( |(B, C)| - |(C, C)|) - |(A, B)|) + |(A, C)|))) by Th13

      .= (( - |((C - A), (B - C))|) / ( |((B - C), (B - C))| + |((C - A), (B - C))|)) by Th13

      .= (( - |((C - A), (B - C))|) / |((B - C), (B - A))|) by Th13;

      

       A13: (s * rCA) = ( - ((((( |(C, A)| - |(A, A)|) - |(B, C)|) + |(B, A)|) / rCA) * rCA)) by A6

      .= ( - ((( |(C, A)| - |(A, A)|) - |(B, C)|) + |(B, A)|)) by A9, EUCLID_4: 17, XCMPLX_1: 87;

      (s / (1 - s)) = (((s / (1 - s)) * rCA) / rCA) by A9, EUCLID_4: 17, XCMPLX_1: 89

      .= (((s * rCA) / (1 - s)) / rCA)

      .= ((s * rCA) / ((1 - s) * rCA)) by XCMPLX_1: 78

      .= (( - ((( |(C, A)| - |(A, A)|) - |(B, C)|) + |(B, A)|)) / ( |((C - A), (C - A))| + ((( |(C, A)| - |(A, A)|) - |(B, C)|) + |(B, A)|))) by A13;

      

      then

       A14: (s / (1 - s)) = (( - |((C - A), (A - B))|) / ( |((C - A), (C - A))| + ((( |(C, A)| - |(A, A)|) - |(B, C)|) + |(B, A)|))) by Th13

      .= (( - |((C - A), (A - B))|) / ( |((C - A), (C - A))| + |((C - A), (A - B))|)) by Th13

      .= (( - |((C - A), (A - B))|) / |((C - A), (C - B))|) by Th13;

      

       A15: (t * rAB) = ( - ((((( |(A, B)| - |(B, B)|) - |(C, A)|) + |(C, B)|) / rAB) * rAB)) by A7

      .= ( - ((( |(A, B)| - |(B, B)|) - |(C, A)|) + |(C, B)|)) by A10, EUCLID_4: 17, XCMPLX_1: 87;

      (t / (1 - t)) = (((t / (1 - t)) * rAB) / rAB) by A10, EUCLID_4: 17, XCMPLX_1: 89

      .= (((t * rAB) / (1 - t)) / rAB)

      .= ((t * rAB) / ((1 - t) * rAB)) by XCMPLX_1: 78

      .= (( - ((( |(A, B)| - |(B, B)|) - |(C, A)|) + |(C, B)|)) / ( |((A - B), (A - B))| + ((( |(A, B)| - |(B, B)|) - |(C, A)|) + |(C, B)|))) by A15;

      

      then

       A16: (t / (1 - t)) = (( - |((A - B), (B - C))|) / ( |((A - B), (A - B))| + ((( |(A, B)| - |(B, B)|) - |(C, A)|) + |(C, B)|))) by Th13

      .= (( - |((A - B), (B - C))|) / ( |((A - B), (A - B))| + |((A - B), (B - C))|)) by Th13

      .= (( - |((A - B), (B - C))|) / |((A - B), (A - C))|) by Th13;

      (((((r / (1 - r)) * s) / (1 - s)) * t) / (1 - t)) = (((( - |((C - A), (B - C))|) / |((B - C), (B - A))|) * (( - |((C - A), (A - B))|) / |((C - A), (C - B))|)) * (( - |((A - B), (B - C))|) / |((A - B), (A - C))|)) by A12, A14, A16

      .= (((( - |((C - A), (B - C))|) / ( - |((B - C), (A - B))|)) * (( - |((C - A), (A - B))|) / |((C - A), (C - B))|)) * (( - |((A - B), (B - C))|) / |((A - B), (A - C))|)) by Th14

      .= (((( - |((C - A), (B - C))|) / ( - |((B - C), (A - B))|)) * (( - |((C - A), (A - B))|) / ( - |((C - A), (B - C))|))) * (( - |((A - B), (B - C))|) / |((A - B), (A - C))|)) by Th14

      .= (((( - |((C - A), (B - C))|) / ( - |((B - C), (A - B))|)) * (( - |((C - A), (A - B))|) / ( - |((C - A), (B - C))|))) * (( - |((B - C), (A - B))|) / ( - |((C - A), (A - B))|))) by Th14

      .= 1 by A4, Th3;

      hence thesis;

    end;

    theorem :: EUCLID13:19

    Cn = ((r * An) + ((1 - r) * Bn)) & r = 1 implies Cn = An

    proof

      assume that

       A1: Cn = ((r * An) + ((1 - r) * Bn)) and

       A2: r = 1;

      reconsider rA = An, rB = Bn, rC = Cn as Element of ( REAL n) by EUCLID: 22;

      rC = (rA + ( 0 * rB)) by A1, A2, EUCLID_4: 3;

      then rC = (rA + ( 0* n)) by EUCLID_4: 3;

      hence thesis by EUCLID_4: 1;

    end;

    theorem :: EUCLID13:20

    Cn = ((r * An) + ((1 - r) * Bn)) & r = 0 implies Cn = Bn

    proof

      assume that

       A1: Cn = ((r * An) + ((1 - r) * Bn)) and

       A2: r = 0 ;

      reconsider rA = An, rB = Bn, rC = Cn as Element of ( REAL n) by EUCLID: 22;

      rC = (( 0 * rA) + ((1 - 0 ) * rB)) by A1, A2;

      then rC = (( 0* n) + (1 * rB)) by EUCLID_4: 3;

      then rC = (1 * rB) by EUCLID_4: 1;

      hence thesis by EUCLID_4: 3;

    end;

    theorem :: EUCLID13:21

    

     Th18: |((Bn - Cn), (Bn - Cn))| = ( - |((Cn - An), (Bn - Cn))|) implies |((Bn - Cn), (An - Bn))| = 0

    proof

      assume

       A1: |((Bn - Cn), (Bn - Cn))| = ( - |((Cn - An), (Bn - Cn))|);

      reconsider rA = An, rB = Bn, rC = Cn as Element of ( REAL n) by EUCLID: 22;

      ( |((rB - rC), (rB - rC))| + |((rB - rC), (rC - rA))|) = 0 by A1;

      then |((rB - rC), ((rB - rC) + (rC - rA)))| = 0 by EUCLID_4: 28;

      then |((rB - rC), (((rB - rC) + rC) - rA))| = 0 by RVSUM_1: 40;

      then |((Bn - Cn), (Bn - An))| = 0 by RVSUM_1: 43;

      then ( - |((Bn - Cn), (An - Bn))|) = 0 by Th14;

      hence thesis;

    end;

    theorem :: EUCLID13:22

    

     Th19: Bn <> Cn & r = ( - (((( |(Bn, Cn)| - |(Cn, Cn)|) - |(An, Bn)|) + |(An, Cn)|) / |((Bn - Cn), (Bn - Cn))|)) & r = 1 implies |((Bn - Cn), (An - Bn))| = 0

    proof

      assume that

       A1: Bn <> Cn and

       A2: r = ( - (((( |(Bn, Cn)| - |(Cn, Cn)|) - |(An, Bn)|) + |(An, Cn)|) / |((Bn - Cn), (Bn - Cn))|)) and

       A3: r = 1;

      set A = An, B = Bn, C = Cn;

      reconsider rB = B, rC = C as Element of ( REAL n) by EUCLID: 22;

      

       A4: (rB - rC) <> ( 0* n) by A1, EUCLIDLP: 9;

      (1 * |((B - C), (B - C))|) = (( - ( |((C - A), (B - C))| / |((B - C), (B - C))|)) * |((B - C), (B - C))|) by A3, A2, Th13;

      then |((B - C), (B - C))| = ( - (( |((C - A), (B - C))| / |((B - C), (B - C))|) * |((B - C), (B - C))|));

      then |((B - C), (B - C))| = ( - |((C - A), (B - C))|) by A4, EUCLID_4: 17, XCMPLX_1: 87;

      hence thesis by Th18;

    end;

    theorem :: EUCLID13:23

    A <> B & A <> C implies ( |.(A - B).| + |.(A - C).|) <> 0

    proof

      assume A <> B & A <> C;

      then |.(A - B).| <> 0 & |.(A - C).| <> 0 by EUCLID_6: 42;

      hence thesis;

    end;

    theorem :: EUCLID13:24

    

     Th20: (A,B,C) is_a_triangle implies not A in ( Line (B,C))

    proof

      assume

       A1: (A,B,C) is_a_triangle ;

      then

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

      assume A in ( Line (B,C));

      hence thesis by A1, A2, MENELAUS: 13;

    end;

    theorem :: EUCLID13:25

    A <> B & B <> C & |((B - A), (B - C))| = 0 implies ( angle (A,B,C)) = ( PI / 2) or ( angle (A,B,C)) = ((3 / 2) * PI )

    proof

      assume that

       A1: A <> B and

       A2: B <> C and

       A3: |((B - A), (B - C))| = 0 ;

       |((A - B), (C - B))| = |(( - (A - B)), ( - (C - B)))| by EUCLID_2: 23

      .= |((B - A), ( - (C - B)))| by RVSUM_1: 35

      .= 0 by A3, RVSUM_1: 35;

      hence thesis by A1, A2, EUCLID_3: 45;

    end;

    theorem :: EUCLID13:26

    

     Th21: (A,B,C) is_a_triangle implies ( sin (( angle (A,B,C)) / 2)) > 0

    proof

      assume

       A1: (A,B,C) is_a_triangle ;

       0 <= ( angle (A,B,C)) < (2 * PI ) by EUCLID11: 2;

      then 0 < ( angle (A,B,C)) < (2 * PI ) by A1, EUCLID10: 30;

      then ( 0 / 2) < (( angle (A,B,C)) / 2) < ((2 * PI ) / 2) by XREAL_1: 74;

      then ((2 * PI ) * 0 ) < (( angle (A,B,C)) / 2) < ( PI + ((2 * PI ) * 0 ));

      hence thesis by SIN_COS6: 11;

    end;

    theorem :: EUCLID13:27

    ( angle (B,A,C)) <> ( angle (C,B,A)) implies ( sin ((( angle (B,A,C)) - ( angle (C,B,A))) / 2)) <> 0

    proof

      assume

       A1: ( angle (B,A,C)) <> ( angle (C,B,A));

      assume

       A2: ( sin ((( angle (B,A,C)) - ( angle (C,B,A))) / 2)) = 0 ;

      then

      consider i0 be Integer such that

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

      set a = (( angle (B,A,C)) - ( angle (C,B,A)));

      

       A4: 0 <= ( angle (B,A,C)) < (2 * PI ) & 0 <= ( angle (C,B,A)) < (2 * PI ) by EUCLID11: 2;

      

       A5: ( 0 - (2 * PI )) < ( 0 - ( angle (C,B,A))) by EUCLID11: 2, XREAL_1: 10;

      per cases ;

        suppose i0 = 0 ;

        hence contradiction by A3, A1;

      end;

        suppose

         A6: i0 < 0 ;

         PI in ]. 0 , 4.[ by SIN_COS:def 28;

        then 0 < PI by XXREAL_1: 4;

        then

         A7: a < 0 by A3, A6;

        ( - (2 * PI )) < a by A5, EUCLID11: 2, XREAL_1: 8;

        hence contradiction by A2, A7, Th5;

      end;

        suppose

         A8: i0 > 0 ;

         0 < a < (2 * PI )

        proof

          thus 0 < a by A3, A8, COMPTRIG: 5;

          (( angle (B,A,C)) - ( angle (C,B,A))) < ((2 * PI ) - 0 ) by A4, XREAL_1: 14;

          hence a < (2 * PI );

        end;

        hence contradiction by A2, Th4;

      end;

    end;

    theorem :: EUCLID13:28

    

     Th22: (A,B,C) is_a_triangle implies ( sin ( angle (A,B,C))) <> 0

    proof

      assume

       A1: (A,B,C) is_a_triangle ;

      assume

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

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

      .= 0 by A2;

      then not (C,B,A) is_a_triangle by MENELAUS: 9;

      hence thesis by A1, MENELAUS: 15;

    end;

    theorem :: EUCLID13:29

    

     Th23: (A,C,B) is_a_triangle & ( angle (A,C,B)) < PI implies ( angle (A,C,B)) = ( PI - (( angle (C,B,A)) + ( angle (B,A,C))))

    proof

      assume that

       A1: (A,C,B) is_a_triangle and

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

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

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

      hence thesis;

    end;

    theorem :: EUCLID13:30

    

     Th24: (A,C,B) is_a_triangle & ( angle (A,C,B)) < PI implies (( angle (B,A,C)) + ( angle (C,B,A))) = ( PI - ( angle (A,C,B)))

    proof

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

      then ( angle (A,C,B)) = ( PI - (( angle (C,B,A)) + ( angle (B,A,C)))) by Th23;

      hence thesis;

    end;

    theorem :: EUCLID13:31

    

     Th25: (A,B,C) is_a_triangle implies (( angle (B,A,C)) - ( angle (C,B,A))) <> PI

    proof

      assume

       A1: (A,B,C) is_a_triangle ;

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

      then

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

      assume

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

      per cases by EUCLID11: 3;

        suppose

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

        (( angle (B,A,C)) - PI ) = ( angle (C,B,A)) by A2;

        hence contradiction by A3, XREAL_1: 49, EUCLID11: 2;

      end;

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

        then ( angle (C,B,A)) = 0 by A2;

        hence contradiction by A1, EUCLID10: 30;

      end;

        suppose

         A4: PI < ( angle (B,A,C)) < (2 * PI );

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

        hence contradiction by A1A, A2, A4, EUCLID11: 8;

      end;

    end;

    theorem :: EUCLID13:32

    

     Th26: (A,B,C) is_a_triangle implies (( angle (B,A,C)) - ( angle (C,B,A))) <> ( - PI )

    proof

      assume

       A1: (A,B,C) is_a_triangle ;

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

      then

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

      assume

       A3: (( angle (B,A,C)) - ( angle (C,B,A))) = ( - PI );

      per cases by EUCLID11: 3;

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

        then

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

        then ( 0 + PI ) < (( angle (B,A,C)) + PI ) by XREAL_1: 8;

        hence contradiction by A3, A4, A2, EUCLID11: 5;

      end;

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

        hence contradiction by A3, EUCLID11: 2;

      end;

        suppose PI < ( angle (B,A,C)) < (2 * PI );

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

        hence contradiction by A3, EUCLID11: 2;

      end;

    end;

    theorem :: EUCLID13:33

    

     Th27: (A,B,C) is_a_triangle implies (( - 2) * PI ) < (( angle (B,A,C)) - ( angle (C,B,A))) < (2 * PI )

    proof

      assume

       A1: (A,B,C) is_a_triangle ;

      

       A2: 0 <= ( angle (B,A,C)) < (2 * PI ) & 0 <= ( angle (C,B,A)) < (2 * PI ) by EUCLID11: 2;

      then

       A3: 0 < ( angle (B,A,C)) < (2 * PI ) & 0 < ( angle (C,B,A)) < (2 * PI ) by A1, EUCLID10: 30;

      ( 0 - (2 * PI )) < (( angle (B,A,C)) - ( angle (C,B,A))) by A3, XREAL_1: 14;

      hence (( - 2) * PI ) < (( angle (B,A,C)) - ( angle (C,B,A)));

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

      hence thesis;

    end;

    theorem :: EUCLID13:34

    (A,B,C) is_a_triangle implies ( - PI ) < ((( angle (B,A,C)) - ( angle (C,B,A))) / 2) < PI

    proof

      assume (A,B,C) is_a_triangle ;

      then (( - 2) * PI ) < (( angle (B,A,C)) - ( angle (C,B,A))) < (2 * PI ) by Th27;

      then ((( - 2) * PI ) / 2) < ((( angle (B,A,C)) - ( angle (C,B,A))) / 2) < ((2 * PI ) / 2) by XREAL_1: 74;

      hence thesis;

    end;

    theorem :: EUCLID13:35

    

     Th28: (A,B,C) is_a_triangle & ( angle (B,A,C)) < PI implies ( - PI ) < (( angle (B,A,C)) - ( angle (C,B,A))) < PI

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

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

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

      then

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

      

       A4: 0 <= ( angle (B,A,C)) & ( angle (B,A,C)) is non zero by A1, EUCLID10: 30, EUCLID11: 2;

      

       A5: 0 <= ( angle (B,A,C)) < PI & 0 <= ( angle (C,B,A)) < PI by A2, A4, A3, EUCLID11: 5;

      

       A6: 0 < ( angle (B,A,C)) < PI & 0 < ( angle (C,B,A)) < PI by A2, A4, A3, EUCLID11: 5;

      ( 0 - PI ) < (( angle (B,A,C)) - ( angle (C,B,A))) by A6, XREAL_1: 14;

      hence ( - PI ) < (( angle (B,A,C)) - ( angle (C,B,A)));

      (( angle (B,A,C)) - ( angle (C,B,A))) < ( PI - 0 ) by A5, XREAL_1: 14;

      hence thesis;

    end;

    theorem :: EUCLID13:36

    

     Th29: (A,B,C) is_a_triangle & ( angle (B,A,C)) < PI implies ( - ( PI / 2)) < ((( angle (B,A,C)) - ( angle (C,B,A))) / 2) < ( PI / 2)

    proof

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

      then ( - PI ) < (( angle (B,A,C)) - ( angle (C,B,A))) < PI by Th28;

      then (( - PI ) / 2) < ((( angle (B,A,C)) - ( angle (C,B,A))) / 2) < ( PI / 2) by XREAL_1: 74;

      hence thesis;

    end;

    begin

    reserve D for Point of ( TOP-REAL 2);

    reserve a,b,c,d for Real;

    definition

      let A,B,C be Point of ( TOP-REAL 2);

      assume

       A1: B <> C;

      :: EUCLID13:def1

      func the_altitude (A,B,C) -> Element of ( line_of_REAL 2) means

      : Def1: ex L1,L2 be Element of ( line_of_REAL 2) st it = L1 & L2 = ( Line (B,C)) & A in L1 & L1 _|_ L2;

      existence

      proof

        reconsider rA = A, rB = B, rC = C as Element of ( REAL 2) by EUCLID: 22;

        reconsider L2 = ( Line (rB,rC)) as Element of ( line_of_REAL 2) by EUCLIDLP: 47;

        L2 is being_line by A1;

        then

        consider L1 be Element of ( line_of_REAL 2) such that

         A2: rA in L1 and

         A3: L2 _|_ L1 by EUCLID12: 47;

        L2 = ( Line (B,C)) by EUCLID12: 4;

        hence thesis by A2, A3;

      end;

      uniqueness

      proof

        let L1,L2 be Element of ( line_of_REAL 2) such that

         A4: ex L11,L12 be Element of ( line_of_REAL 2) st L1 = L11 & L12 = ( Line (B,C)) & A in L11 & L11 _|_ L12 and

         A5: ex L21,L22 be Element of ( line_of_REAL 2) st L2 = L21 & L22 = ( Line (B,C)) & A in L21 & L21 _|_ L22;

        consider L11,L12 be Element of ( line_of_REAL 2) such that

         A6: L1 = L11 and

         A7: L12 = ( Line (B,C)) and

         A8: A in L11 and

         A9: L11 _|_ L12 by A4;

        consider L21,L22 be Element of ( line_of_REAL 2) such that

         A10: L2 = L21 and

         A11: L22 = ( Line (B,C)) and

         A12: A in L21 and

         A13: L21 _|_ L22 by A5;

         not L11 misses L21 by A8, A12, XBOOLE_0:def 4;

        hence thesis by A6, A10, EUCLIDLP: 71, A7, A11, EUCLID12: 16, A9, A13, EUCLIDLP: 111;

      end;

    end

    theorem :: EUCLID13:37

    

     Th30: B <> C implies A in ( the_altitude (A,B,C))

    proof

      assume B <> C;

      then

      consider L1,L2 be Element of ( line_of_REAL 2) such that

       A1: ( the_altitude (A,B,C)) = L1 and L2 = ( Line (B,C)) and

       A2: A in L1 and L1 _|_ L2 by Def1;

      thus thesis by A1, A2;

    end;

    theorem :: EUCLID13:38

    

     Th31: B <> C implies ( the_altitude (A,B,C)) is being_line

    proof

      assume B <> C;

      then

      consider L1,L2 be Element of ( line_of_REAL 2) such that

       A1: ( the_altitude (A,B,C)) = L1 and L2 = ( Line (B,C)) and A in L1 and

       A2: L1 _|_ L2 by Def1;

      thus thesis by A1, A2, EUCLIDLP: 67;

    end;

    theorem :: EUCLID13:39

    

     Th32: B <> C implies ( the_altitude (A,B,C)) = ( the_altitude (A,C,B))

    proof

      assume

       A1: B <> C;

      then

      consider L11,L12 be Element of ( line_of_REAL 2) such that

       A2: ( the_altitude (A,B,C)) = L11 and

       A3: L12 = ( Line (B,C)) and

       A4: A in L11 and

       A5: L11 _|_ L12 by Def1;

      consider L21,L22 be Element of ( line_of_REAL 2) such that

       A6: ( the_altitude (A,C,B)) = L21 and

       A7: L22 = ( Line (C,B)) and

       A8: A in L21 and

       A9: L21 _|_ L22 by A1, Def1;

      L11 // L21 by A5, A9, A3, A7, EUCLID12: 16, EUCLIDLP: 111;

      hence thesis by A2, A6, A4, A8, XBOOLE_0: 3, EUCLIDLP: 71;

    end;

    theorem :: EUCLID13:40

    B <> C & D in ( the_altitude (A,B,C)) implies ( the_altitude (D,B,C)) = ( the_altitude (A,B,C))

    proof

      assume that

       A1: B <> C and

       A2: D in ( the_altitude (A,B,C));

      consider L1,L2 be Element of ( line_of_REAL 2) such that

       A3: ( the_altitude (A,B,C)) = L1 and

       A4: L2 = ( Line (B,C)) and A in L1 and

       A5: L1 _|_ L2 by A1, Def1;

      consider L11,L12 be Element of ( line_of_REAL 2) such that

       A6: ( the_altitude (D,B,C)) = L11 and

       A7: L12 = ( Line (B,C)) and

       A8: D in L11 and

       A9: L11 _|_ L12 by A1, Def1;

      L1 // L11 & D in L1 & D in L11 by A2, A3, A8, A4, A7, A5, A9, EUCLID12: 16, EUCLIDLP: 111;

      hence thesis by A3, A6, EUCLIDLP: 71, XBOOLE_0: 3;

    end;

    theorem :: EUCLID13:41

    

     Th33: B <> C & D in ( Line (B,C)) & D <> C implies ( the_altitude (A,B,C)) = ( the_altitude (A,D,C))

    proof

      assume that

       A1: B <> C and

       A2: D in ( Line (B,C)) and

       A3: D <> C;

      consider L1,L2 be Element of ( line_of_REAL 2) such that

       A4: ( the_altitude (A,B,C)) = L1 and

       A5: L2 = ( Line (B,C)) and

       A6: A in L1 and

       A7: L1 _|_ L2 by A1, Def1;

      consider L3,L4 be Element of ( line_of_REAL 2) such that

       A8: ( the_altitude (A,D,C)) = L3 and

       A9: L4 = ( Line (D,C)) and

       A10: A in L3 and

       A11: L3 _|_ L4 by A3, Def1;

      

       A12: L2 = L4 by A2, A3, A5, A9, Th7;

      L1 meets L3 by A6, A10, XBOOLE_0:def 4;

      hence thesis by A4, A8, A7, A11, A12, EUCLIDLP: 111, EUCLID12: 16, EUCLIDLP: 71;

    end;

    definition

      let A,B,C be Point of ( TOP-REAL 2);

      assume

       A1: B <> C;

      :: EUCLID13:def2

      func the_foot_of_the_altitude (A,B,C) -> Point of ( TOP-REAL 2) means

      : Def2: ex P be Point of ( TOP-REAL 2) st it = P & (( the_altitude (A,B,C)) /\ ( Line (B,C))) = {P};

      existence

      proof

        consider L1,L2 be Element of ( line_of_REAL 2) such that

         A2: ( the_altitude (A,B,C)) = L1 and

         A3: L2 = ( Line (B,C)) and A in L1 and

         A4: L1 _|_ L2 by A1, Def1;

        consider x be Element of ( REAL 2) such that

         A5: (L1 /\ L2) = {x} by A4, EUCLID12: 43;

        reconsider P = x as Point of ( TOP-REAL 2) by EUCLID: 22;

        take P;

        thus thesis by A2, A3, A5;

      end;

      uniqueness by ZFMISC_1: 3;

    end

    theorem :: EUCLID13:42

    

     Th34: B <> C implies ( the_foot_of_the_altitude (A,B,C)) = ( the_foot_of_the_altitude (A,C,B))

    proof

      assume

       A1: B <> C;

      consider D be Point of ( TOP-REAL 2) such that

       A2: ( the_foot_of_the_altitude (A,B,C)) = D and

       A3: (( the_altitude (A,B,C)) /\ ( Line (B,C))) = {D} by A1, Def2;

      consider E be Point of ( TOP-REAL 2) such that

       A4: ( the_foot_of_the_altitude (A,C,B)) = E and

       A5: (( the_altitude (A,C,B)) /\ ( Line (C,B))) = {E} by A1, Def2;

       {D} = {E} by A3, A5, A1, Th32;

      hence thesis by A2, A4, ZFMISC_1: 3;

    end;

    theorem :: EUCLID13:43

    

     Th35: B <> C implies ( the_foot_of_the_altitude (A,B,C)) in ( Line (B,C)) & ( the_foot_of_the_altitude (A,B,C)) in ( the_altitude (A,B,C))

    proof

      assume B <> C;

      then

      consider P be Point of ( TOP-REAL 2) such that

       A1: P = ( the_foot_of_the_altitude (A,B,C)) and

       A2: (( the_altitude (A,B,C)) /\ ( Line (B,C))) = {P} by Def2;

      P in {P} by TARSKI:def 1;

      hence thesis by A1, A2, XBOOLE_0:def 4;

    end;

    theorem :: EUCLID13:44

    

     Th36: B <> C & not A in ( Line (B,C)) implies ( the_altitude (A,B,C)) = ( Line (A,( the_foot_of_the_altitude (A,B,C))))

    proof

      assume that

       A1: B <> C and

       A2: not A in ( Line (B,C));

      consider L1,L2 be Element of ( line_of_REAL 2) such that

       A3: ( the_altitude (A,B,C)) = L1 and

       A4: L2 = ( Line (B,C)) and

       A5: A in L1 and

       A6: L1 _|_ L2 by A1, Def1;

      consider P be Point of ( TOP-REAL 2) such that

       A7: ( the_foot_of_the_altitude (A,B,C)) = P and

       A8: (( the_altitude (A,B,C)) /\ ( Line (B,C))) = {P} by A1, Def2;

      reconsider rA = A, rP = P as Element of ( REAL 2) by EUCLID: 22;

      reconsider L3 = ( Line (rA,rP)) as Element of ( line_of_REAL 2) by EUCLIDLP: 47;

      per cases ;

        suppose A = P;

        then A in (( the_altitude (A,B,C)) /\ ( Line (B,C))) by A8, TARSKI:def 1;

        hence thesis by A2, XBOOLE_0:def 4;

      end;

        suppose

         A9: A <> P;

        A in L1 & P in L1 & L1 is being_line by A6, A3, A5, A1, A7, Th35, EUCLIDLP: 67;

        then ( Line (A,P)) = L1 by A9, EUCLID12: 49;

        then A in L3 & L3 _|_ L2 by A6, EUCLID12: 4, EUCLID_4: 9;

        then L3 = ( the_altitude (A,B,C)) & L3 = ( Line (A,P)) by A1, A4, Def1, EUCLID12: 4;

        hence thesis by A7;

      end;

    end;

    theorem :: EUCLID13:45

    

     Th37: B <> C & A in ( Line (B,C)) implies ( the_foot_of_the_altitude (A,B,C)) = A

    proof

      assume that

       A1: B <> C and

       A2: A in ( Line (B,C));

      consider P be Point of ( TOP-REAL 2) such that

       A3: ( the_foot_of_the_altitude (A,B,C)) = P and

       A4: (( the_altitude (A,B,C)) /\ ( Line (B,C))) = {P} by A1, Def2;

      consider L1,L2 be Element of ( line_of_REAL 2) such that

       A5: ( the_altitude (A,B,C)) = L1 and

       A6: L2 = ( Line (B,C)) and

       A7: A in L1 and L1 _|_ L2 by A1, Def1;

      A in (L1 /\ L2) by A6, A7, A2, XBOOLE_0:def 4;

      hence thesis by A3, A4, A5, A6, TARSKI:def 1;

    end;

    theorem :: EUCLID13:46

    B <> C & ( the_foot_of_the_altitude (A,B,C)) = A implies A in ( Line (B,C)) by Th35;

    theorem :: EUCLID13:47

    

     Th38ThJ8: B <> C implies |((A - ( the_foot_of_the_altitude (A,B,C))), (B - C))| = 0

    proof

      assume

       A1: B <> C;

      consider L1,L2 be Element of ( line_of_REAL 2) such that

       A2: ( the_altitude (A,B,C)) = L1 and

       A3: L2 = ( Line (B,C)) & A in L1 & L1 _|_ L2 by A1, Def1;

      per cases ;

        suppose not A in ( Line (B,C));

        then L1 _|_ L2 & L1 = ( Line (A,( the_foot_of_the_altitude (A,B,C)))) & L2 = ( Line (B,C)) by A1, A2, A3, Th36;

        hence thesis by EUCLID12: 48;

      end;

        suppose A in ( Line (B,C));

        then

         A4: ( the_foot_of_the_altitude (A,B,C)) = A by A1, Th37;

         |((A - ( the_foot_of_the_altitude (A,B,C))), (B - C))| = ( |(A, (B - C))| - |(( the_foot_of_the_altitude (A,B,C)), (B - C))|) by EUCLID_2: 27

        .= 0 by A4;

        hence thesis;

      end;

    end;

    theorem :: EUCLID13:48

    

     Th39: B <> C implies |((A - ( the_foot_of_the_altitude (A,B,C))), (B - ( the_foot_of_the_altitude (A,B,C))))| = 0

    proof

      assume

       A1: B <> C;

      consider L1,L2 be Element of ( line_of_REAL 2) such that

       A2: ( the_altitude (A,B,C)) = L1 and

       A3: L2 = ( Line (B,C)) & A in L1 & L1 _|_ L2 by A1, Def1;

      per cases ;

        suppose

         A4: B = ( the_foot_of_the_altitude (A,B,C));

         |((A - ( the_foot_of_the_altitude (A,B,C))), (B - ( the_foot_of_the_altitude (A,B,C))))| = ( |((A - ( the_foot_of_the_altitude (A,B,C))), B)| - |((A - ( the_foot_of_the_altitude (A,B,C))), ( the_foot_of_the_altitude (A,B,C)))|) by EUCLID_2: 27;

        hence thesis by A4;

      end;

        suppose

         A5: B <> ( the_foot_of_the_altitude (A,B,C));

        

         A6: L2 is being_line by A3, EUCLIDLP: 67;

        ( the_foot_of_the_altitude (A,B,C)) in ( Line (B,C)) & B in ( Line (B,C)) & C in ( Line (B,C)) by EUCLID_4: 41, A1, Th35;

        then

         A7: ( Line (B,C)) = ( Line (B,( the_foot_of_the_altitude (A,B,C)))) by A6, A5, A3, EUCLID12: 49;

        per cases ;

          suppose not A in ( Line (B,C));

          then L1 _|_ L2 & L1 = ( Line (A,( the_foot_of_the_altitude (A,B,C)))) & L2 = ( Line (B,C)) by A1, A2, A3, Th36;

          hence thesis by A7, EUCLID12: 48;

        end;

          suppose A in ( Line (B,C));

          then

           A8: A = ( the_foot_of_the_altitude (A,B,C)) by A1, Th37;

           |((A - ( the_foot_of_the_altitude (A,B,C))), (B - ( the_foot_of_the_altitude (A,B,C))))| = ( |(A, (B - ( the_foot_of_the_altitude (A,B,C))))| - |(( the_foot_of_the_altitude (A,B,C)), (B - ( the_foot_of_the_altitude (A,B,C))))|) by EUCLID_2: 27

          .= 0 by A8;

          hence thesis;

        end;

      end;

    end;

    theorem :: EUCLID13:49

    

     Th40: B <> C implies |((A - ( the_foot_of_the_altitude (A,B,C))), (C - ( the_foot_of_the_altitude (A,B,C))))| = 0

    proof

      assume

       A1: B <> C;

      then ( the_foot_of_the_altitude (A,C,B)) = ( the_foot_of_the_altitude (A,B,C)) by Th34;

      hence thesis by A1, Th39;

    end;

    theorem :: EUCLID13:50

    

     Th41: B <> C & B = ( the_foot_of_the_altitude (A,B,C)) implies |((B - A), (B - C))| = 0

    proof

      assume that

       A1: B <> C and

       A2: B = ( the_foot_of_the_altitude (A,B,C));

      set ph = ( the_foot_of_the_altitude (A,B,C));

      per cases ;

        suppose (A,B,C) is_a_triangle ;

         |((A - ph), (C - ph))| = 0 by A1, Th40;

        hence thesis by A2, Th10;

      end;

        suppose

         A4: not (A,B,C) is_a_triangle ;

        consider P be Point of ( TOP-REAL 2) such that

         A5: ( the_foot_of_the_altitude (A,B,C)) = P and

         A6: (( the_altitude (A,B,C)) /\ ( Line (B,C))) = {P} by A1, Def2;

        consider L1,L2 be Element of ( line_of_REAL 2) such that

         A7: ( the_altitude (A,B,C)) = L1 and L2 = ( Line (B,C)) and

         A8: A in L1 and L1 _|_ L2 by A1, Def1;

        A in ( Line (B,C)) & B in ( Line (B,C)) & A in ( the_altitude (A,B,C)) & B in ( the_altitude (A,B,C)) by A1, A4, MENELAUS: 13, A7, A8, Th35, A2;

        then A in {( the_foot_of_the_altitude (A,B,C))} by A5, A6, XBOOLE_0:def 4;

        then

         A11: A = B by A2, TARSKI:def 1;

         |((B - A), (B - C))| = ( |(B, (B - C))| - |(A, (B - C))|) by EUCLID_2: 24

        .= 0 by A11;

        hence thesis;

      end;

    end;

    theorem :: EUCLID13:51

    

     Th42: B <> C & D in ( Line (B,C)) & D <> C implies ( the_foot_of_the_altitude (A,B,C)) = ( the_foot_of_the_altitude (A,D,C))

    proof

      assume that

       A1: B <> C and

       A2: D in ( Line (B,C)) and

       A3: D <> C;

      consider P1 be Point of ( TOP-REAL 2) such that

       A4: ( the_foot_of_the_altitude (A,B,C)) = P1 and

       A5: (( the_altitude (A,B,C)) /\ ( Line (B,C))) = {P1} by A1, Def2;

      consider P2 be Point of ( TOP-REAL 2) such that

       A6: ( the_foot_of_the_altitude (A,D,C)) = P2 and

       A7: (( the_altitude (A,D,C)) /\ ( Line (D,C))) = {P2} by A3, Def2;

      ( Line (D,C)) = ( Line (B,C)) by A2, A3, Th7;

      then {P1} = {P2} by A7, A5, A1, A2, A3, Th33;

      hence thesis by A4, A6, ZFMISC_1: 3;

    end;

    theorem :: EUCLID13:52

    

     Th43: B <> C & |((B - A), (B - C))| = 0 implies B = ( the_foot_of_the_altitude (A,B,C))

    proof

      assume that

       A1: B <> C and

       A2: |((B - A), (B - C))| = 0 ;

      set p = ( the_foot_of_the_altitude (A,B,C));

      consider P be Point of ( TOP-REAL 2) such that

       A3: p = P and

       A4: (( the_altitude (A,B,C)) /\ ( Line (B,C))) = {P} by A1, Def2;

      consider L1,L2 be Element of ( line_of_REAL 2) such that

       A5: ( the_altitude (A,B,C)) = L1 and

       A6: L2 = ( Line (B,C)) and

       A7: A in L1 and

       A8: L1 _|_ L2 by A1, Def1;

      per cases ;

        suppose

         A9: A = p;

        A = B

        proof

          assume

           A10: A <> B;

          reconsider rA = A, rB = B, rC = C as Element of ( REAL 2) by EUCLID: 22;

          reconsider LBA = ( Line (rB,rA)), LBC = ( Line (rB,rC)) as Element of ( line_of_REAL 2) by EUCLIDLP: 47;

          

           A11: ( Line (B,A)) = ( Line (rB,rA)) by EUCLID12: 4;

          then A in LBA & B in LBA by EUCLID_4: 41;

          then

           A12: L1 meets LBA by A7, XBOOLE_0:def 4;

          A <> B & B <> C & |((B - A), (B - C))| = 0 & LBA = ( Line (B,A)) & LBC = ( Line (B,C)) by A1, A2, A10, EUCLID12: 4;

          then LBA _|_ LBC & L1 _|_ LBC & LBA c= ( REAL 2) & L1 c= ( REAL 2) & LBC c= ( REAL 2) by A6, A8, Th9;

          then LBA = L1 by EUCLIDLP: 111, EUCLID12: 16, A12, EUCLIDLP: 71;

          then B in L1 & B in L2 by A6, A11, EUCLID_4: 41;

          then B in {P} by A4, A5, A6, XBOOLE_0:def 4;

          hence contradiction by A10, A9, A3, TARSKI:def 1;

        end;

        hence thesis by A9;

      end;

        suppose

         A13: A <> p;

        

         A14: A <> B

        proof

          assume A = B;

          then A in ( Line (B,C)) by EUCLID_4: 41;

          hence contradiction by A13, A1, Th37;

        end;

        reconsider rA = A, rB = B, rC = C as Element of ( REAL 2) by EUCLID: 22;

        reconsider LBA = ( Line (rB,rA)), LBC = ( Line (rB,rC)) as Element of ( line_of_REAL 2) by EUCLIDLP: 47;

        

         A15: ( Line (B,A)) = ( Line (rB,rA)) by EUCLID12: 4;

        then A in LBA & B in LBA by EUCLID_4: 41;

        then

         A16: L1 meets LBA by A7, XBOOLE_0:def 4;

        A <> B & B <> C & |((B - A), (B - C))| = 0 & LBA = ( Line (B,A)) & LBC = ( Line (B,C)) by A1, A2, A14, EUCLID12: 4;

        then LBA _|_ LBC & L1 _|_ LBC & LBA c= ( REAL 2) & L1 c= ( REAL 2) & LBC c= ( REAL 2) by A6, A8, Th9;

        then LBA = L1 by EUCLIDLP: 111, EUCLID12: 16, A16, EUCLIDLP: 71;

        then B in L1 & B in L2 by A6, A15, EUCLID_4: 41;

        then B in {P} by A4, A5, A6, XBOOLE_0:def 4;

        hence thesis by A3, TARSKI:def 1;

      end;

    end;

    theorem :: EUCLID13:53

    B <> C & B <> A & ( angle (A,B,C)) = ( PI / 2) implies ( the_foot_of_the_altitude (A,B,C)) = B

    proof

      assume that

       A1: B <> C and

       A2: B <> A and

       A3: ( angle (A,B,C)) = ( PI / 2);

       |((A - B), (C - B))| = 0 by A1, A2, A3, EUCLID_3: 45;

      then |((B - A), (B - C))| = 0 by Th10;

      hence thesis by A1, Th43;

    end;

    theorem :: EUCLID13:54

    

     Th44: (A,B,C) is_a_triangle implies A <> ( the_foot_of_the_altitude (A,B,C))

    proof

      assume

       A1: (A,B,C) is_a_triangle ;

      assume

       A2: A = ( the_foot_of_the_altitude (A,B,C));

      

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

      then A in ( Line (B,C)) by A2, Th35;

      hence contradiction by A1, A3, MENELAUS: 13;

    end;

    theorem :: EUCLID13:55

    

     Th45: (A,B,C) is_a_triangle & |((B - A), (B - C))| <> 0 implies (( the_foot_of_the_altitude (A,B,C)),B,A) is_a_triangle

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: |((B - A), (B - C))| <> 0 ;

      

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

      set p = ( the_foot_of_the_altitude (A,B,C));

      consider P be Point of ( TOP-REAL 2) such that

       A4: ( the_foot_of_the_altitude (A,B,C)) = P and

       A5: (( the_altitude (A,B,C)) /\ ( Line (B,C))) = {P} by A3, Def2;

      consider L1,L2 be Element of ( line_of_REAL 2) such that

       A6: ( the_altitude (A,B,C)) = L1 and

       A7: L2 = ( Line (B,C)) and

       A8: A in L1 and L1 _|_ L2 by A3, Def1;

      

       A9: P <> B by A4, A3, A2, Th41;

      

       A10: p <> A by A1, Th44;

      

       A11: (p,B,A) are_mutually_distinct by A3, A2, Th41, A1, Th44;

      P in ( Line (B,C)) by A4, A3, Th35;

      then B in ( Line (B,P)) & C in ( Line (B,P)) by A9, Th8, EUCLID_4: 41;

      then

       A12: ( Line (B,P)) c= ( Line (B,C)) by A3, EUCLID_4: 43;

      

       A13: ( angle (p,B,A)) <> PI

      proof

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

        then B in ( LSeg (p,A)) by EUCLID_6: 11;

        then B in ( Line (P,A)) by A4, MENELAUS: 12;

        then A in ( Line (B,P)) by A3, A2, Th41, A4, Th8;

        then A in (L1 /\ L2) by A12, A8, A7, XBOOLE_0:def 4;

        hence contradiction by A5, A6, A7, A4, A10, TARSKI:def 1;

      end;

      

       A14: ( angle (B,A,p)) <> PI

      proof

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

        then A in ( LSeg (B,p)) by EUCLID_6: 11;

        then A in L1 & A in L2 by A12, A8, A7, A4, MENELAUS: 12;

        then A in (L1 /\ L2) by XBOOLE_0:def 4;

        hence contradiction by A4, A10, A5, A6, A7, TARSKI:def 1;

      end;

      ( angle (A,p,B)) <> PI

      proof

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

        then p in ( LSeg (A,B)) by EUCLID_6: 11;

        then P in ( Line (A,B)) by A4, MENELAUS: 12;

        then A in ( Line (B,P)) by A9, Th8;

        then A in (L1 /\ L2) by A12, A8, A7, XBOOLE_0:def 4;

        then A = P by A5, A6, A7, TARSKI:def 1;

        hence contradiction by A4, A1, Th44;

      end;

      hence thesis by A11, A13, A14, EUCLID_6: 20;

    end;

    definition

      let A,B,C be Point of ( TOP-REAL 2);

      assume B <> C;

      :: EUCLID13:def3

      func the_length_of_the_altitude (A,B,C) -> Real equals

      : Def3: |.(A - ( the_foot_of_the_altitude (A,B,C))).|;

      correctness ;

    end

    theorem :: EUCLID13:56

    

     Th46: B <> C implies 0 <= ( the_length_of_the_altitude (A,B,C))

    proof

      assume B <> C;

      then ( the_length_of_the_altitude (A,B,C)) = |.(A - ( the_foot_of_the_altitude (A,B,C))).| by Def3;

      hence thesis;

    end;

    theorem :: EUCLID13:57

    B <> C implies ( the_length_of_the_altitude (A,B,C)) = ( the_length_of_the_altitude (A,C,B))

    proof

      assume

       A1: B <> C;

      

      then ( the_length_of_the_altitude (A,B,C)) = |.(A - ( the_foot_of_the_altitude (A,B,C))).| by Def3

      .= |.(A - ( the_foot_of_the_altitude (A,C,B))).| by A1, Th34

      .= ( the_length_of_the_altitude (A,C,B)) by A1, Def3;

      hence thesis;

    end;

    theorem :: EUCLID13:58

    

     Th47: B <> C & |((B - A), (B - C))| = 0 implies |.(( the_foot_of_the_altitude (A,B,C)) - A).| = |.(A - B).|

    proof

      assume that

       A1: B <> C and

       A2: |((B - A), (B - C))| = 0 ;

       |.(( the_foot_of_the_altitude (A,B,C)) - A).| = |.(B - A).| by A1, A2, Th43;

      hence thesis by EUCLID_6: 43;

    end;

    theorem :: EUCLID13:59

    

     Th48: B <> C & r = ( - (((( |(B, C)| - |(C, C)|) - |(A, B)|) + |(A, C)|) / |((B - C), (B - C))|)) & D = ((r * B) + ((1 - r) * C)) & D <> C implies D = ( the_foot_of_the_altitude (A,B,C))

    proof

      assume that

       A1: B <> C and

       A2: r = ( - (((( |(B, C)| - |(C, C)|) - |(A, B)|) + |(A, C)|) / |((B - C), (B - C))|)) and

       A3: D = ((r * B) + ((1 - r) * C)) and

       A4: D <> C;

       |((D - A), (D - C))| = 0 by A1, A2, A3, Th11;

      then

       A5: D = ( the_foot_of_the_altitude (A,D,C)) by A4, Th43;

      reconsider rB = B, rC = C as Element of ( REAL 2) by EUCLID: 22;

      D in ( Line (B,C))

      proof

        D in ( Line (rC,rB)) by A3;

        hence thesis by EUCLID12: 4;

      end;

      hence thesis by A1, A4, A5, Th42;

    end;

    theorem :: EUCLID13:60

    

     Th49: B <> C & r = ( - (((( |(B, C)| - |(C, C)|) - |(A, B)|) + |(A, C)|) / |((B - C), (B - C))|)) & D = ((r * B) + ((1 - r) * C)) & D = C implies C = ( the_foot_of_the_altitude (A,B,C))

    proof

      assume that

       A1: B <> C and

       A2: r = ( - (((( |(B, C)| - |(C, C)|) - |(A, B)|) + |(A, C)|) / |((B - C), (B - C))|)) and

       A3: D = ((r * B) + ((1 - r) * C)) and

       A4: D = C;

      reconsider rB = B, rC = C as Element of ( REAL 2) by EUCLID: 22;

      reconsider n = 2 as Nat;

      

       A5: (rB - rC) <> ( 0* n) by A1, EUCLIDLP: 9;

       0 = ( - (((( |(B, C)| - |(C, C)|) - |(A, B)|) + |(A, C)|) / |((B - C), (B - C))|)) by A2, A1, A3, A4, Th12;

      then ( 0 * |((B - C), (B - C))|) = ( - (( |((C - A), (B - C))| / |((B - C), (B - C))|) * |((B - C), (B - C))|)) by Th13;

      then 0 = ( - |((C - A), (B - C))|) by A5, EUCLID_4: 17, XCMPLX_1: 87;

      then |((C - A), (C - B))| = 0 by Th14;

      then C = ( the_foot_of_the_altitude (A,C,B)) by A1, Th43;

      hence thesis by A1, Th34;

    end;

    theorem :: EUCLID13:61

    

     Th50: (A,B,C) is_a_triangle & |((C - A), (B - C))| is non zero & |((B - C), (A - B))| is non zero & |((C - A), (A - B))| is non zero implies (( Line (A,( the_foot_of_the_altitude (A,B,C)))),( Line (C,( the_foot_of_the_altitude (C,A,B)))),( Line (B,( the_foot_of_the_altitude (B,C,A))))) are_concurrent

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: |((C - A), (B - C))| is non zero & |((B - C), (A - B))| is non zero & |((C - A), (A - B))| is non zero;

      

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

      set r = ( - (((( |(B, C)| - |(C, C)|) - |(A, B)|) + |(A, C)|) / |((B - C), (B - C))|)), s = ( - (((( |(C, A)| - |(A, A)|) - |(B, C)|) + |(B, A)|) / |((C - A), (C - A))|)), t = ( - (((( |(A, B)| - |(B, B)|) - |(C, A)|) + |(C, B)|) / |((A - B), (A - B))|)), D = ((r * B) + ((1 - r) * C)), E = ((s * C) + ((1 - s) * A)), F = ((t * A) + ((1 - t) * B));

      D <> C & E <> A & F <> B

      proof

        assume not (D <> C & E <> A & F <> B);

        then

         A4: C = ( the_foot_of_the_altitude (A,B,C)) or A = ( the_foot_of_the_altitude (B,C,A)) or B = ( the_foot_of_the_altitude (C,A,B)) by A3, Th49;

         |((A - C), (B - C))| = ( - |((C - A), (B - C))|) & |((B - A), (C - A))| = ( - |((C - A), (A - B))|) & |((C - B), (A - B))| = ( - |((B - C), (A - B))|) by Th16;

        hence contradiction by A4, A2, A3, Th38ThJ8;

      end;

      then

       A5: D = ( the_foot_of_the_altitude (A,B,C)) & E = ( the_foot_of_the_altitude (B,C,A)) & F = ( the_foot_of_the_altitude (C,A,B)) by A3, Th48;

      (((((r / (1 - r)) * s) / (1 - s)) * t) / (1 - t)) = 1 by A3, A2, Th17;

      then

       A6: (((r / (1 - r)) * (t / (1 - t))) * (s / (1 - s))) = 1;

      

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

      r <> 1 & s <> 1 & t <> 1

      proof

        assume not (r <> 1 & s <> 1 & t <> 1);

        then (r = 1 & B <> C & r = ( - (((( |(B, C)| - |(C, C)|) - |(A, B)|) + |(A, C)|) / |((B - C), (B - C))|)) & D = ((r * B) + ((1 - r) * C))) or (s = 1 & C <> A & s = ( - (((( |(C, A)| - |(A, A)|) - |(B, C)|) + |(B, A)|) / |((C - A), (C - A))|)) & E = ((s * C) + ((1 - s) * A))) or (t = 1 & A <> B & t = ( - (((( |(A, B)| - |(B, B)|) - |(C, A)|) + |(C, B)|) / |((A - B), (A - B))|)) & F = ((t * A) + ((1 - t) * B)));

        hence contradiction by A2, Th19;

      end;

      hence thesis by A5, A6, A7, MENELAUS: 22;

    end;

    theorem :: EUCLID13:62

    

     Th51: (A,B,C) is_a_triangle & |((C - A), (B - C))| is zero implies ( the_foot_of_the_altitude (A,B,C)) = C & ( the_foot_of_the_altitude (B,C,A)) = C

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: |((C - A), (B - C))| is zero;

      

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

      

       A4: ( - |((C - A), (B - C))|) = |((C - B), (C - A))| by Th14;

       |((C - A), (C - B))| = ( - |((C - A), (B - C))|) by Th14;

      then ( the_foot_of_the_altitude (A,C,B)) = C by A2, A3, Th43;

      hence thesis by A2, A3, A4, Th43, Th34;

    end;

    theorem :: EUCLID13:63

    

     Th52: (A,B,C) is_a_triangle & C in ( the_altitude (A,B,C)) & C in ( the_altitude (B,C,A)) implies (( the_altitude (A,B,C)) /\ ( the_altitude (B,C,A))) is being_point

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: C in ( the_altitude (A,B,C)) and

       A3: C in ( the_altitude (B,C,A));

      

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

      consider L1,L2 be Element of ( line_of_REAL 2) such that

       A5: ( the_altitude (A,B,C)) = L1 and

       A6: L2 = ( Line (B,C)) and A in L1 and

       A7: L1 _|_ L2 by A4, Def1;

      consider L3,L4 be Element of ( line_of_REAL 2) such that

       A8: ( the_altitude (B,C,A)) = L3 and

       A9: L4 = ( Line (C,A)) and B in L3 and

       A10: L3 _|_ L4 by A4, Def1;

      

       A11: not L1 // L3

      proof

        assume

         A12: L1 // L3;

        L1 <> L3

        proof

          assume L1 = L3;

          then L1 _|_ L2 & L1 _|_ L4 & C in L1 & C in L2 & C in L4 by A6, A9, A7, A10, A2, A5, EUCLID_4: 41;

          then L2 = L4 by EUCLID12: 16, EUCLIDLP: 108;

          then A in ( Line (B,C)) by A6, A9, EUCLID_4: 41;

          hence contradiction by A1, A4, MENELAUS: 13;

        end;

        hence contradiction by XBOOLE_0: 3, A12, EUCLIDLP: 71, A5, A8, A2, A3;

      end;

       not L1 is being_point & not L3 is being_point by A4, A5, A8, Th31, EUCLID12: 9;

      hence thesis by A5, A8, A11, EUCLID12: 21;

    end;

    theorem :: EUCLID13:64

    

     Th53: (B,C,A) is_a_triangle & C in ( the_altitude (B,C,A)) & C in ( the_altitude (C,A,B)) implies (( the_altitude (B,C,A)) /\ ( the_altitude (C,A,B))) is being_point

    proof

      assume that

       A1: (B,C,A) is_a_triangle and

       A2: C in ( the_altitude (B,C,A)) and

       A3: C in ( the_altitude (C,A,B));

      

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

      consider L1,L2 be Element of ( line_of_REAL 2) such that

       A5: ( the_altitude (B,C,A)) = L1 and

       A6: L2 = ( Line (C,A)) and B in L1 and

       A7: L1 _|_ L2 by A4, Def1;

      consider L3,L4 be Element of ( line_of_REAL 2) such that

       A8: ( the_altitude (C,A,B)) = L3 and

       A9: L4 = ( Line (A,B)) and C in L3 and

       A10: L3 _|_ L4 by A4, Def1;

      

       A11: not L1 // L3

      proof

        assume L1 // L3;

        then L1 = L3 by EUCLIDLP: 71, A2, A3, A5, A8, XBOOLE_0: 3;

        then

         A12: L2 // L4 by A7, A10, EUCLIDLP: 111, EUCLID12: 16;

        A in L2 & A in L4 by A6, A9, EUCLID_4: 41;

        then ( Line (C,A)) = ( Line (A,B)) by A6, A9, XBOOLE_0: 3, A12, EUCLIDLP: 71;

        then B in ( Line (C,A)) by EUCLID_4: 41;

        hence contradiction by A1, A4, MENELAUS: 13;

      end;

       not L1 is being_point & not L3 is being_point by A4, A5, A8, Th31, EUCLID12: 9;

      hence thesis by A5, A8, A11, EUCLID12: 21;

    end;

    theorem :: EUCLID13:65

    

     Th54: (C,A,B) is_a_triangle & C in ( the_altitude (C,A,B)) & C in ( the_altitude (A,B,C)) implies (( the_altitude (C,A,B)) /\ ( the_altitude (A,B,C))) is being_point

    proof

      assume that

       A1: (C,A,B) is_a_triangle and

       A2: C in ( the_altitude (C,A,B)) and

       A3: C in ( the_altitude (A,B,C));

      

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

      consider L1,L2 be Element of ( line_of_REAL 2) such that

       A5: ( the_altitude (C,A,B)) = L1 and

       A6: L2 = ( Line (A,B)) and C in L1 and

       A7: L1 _|_ L2 by A4, Def1;

      consider L3,L4 be Element of ( line_of_REAL 2) such that

       A8: ( the_altitude (A,B,C)) = L3 and

       A9: L4 = ( Line (B,C)) and A in L3 and

       A10: L3 _|_ L4 by A4, Def1;

      

       A11: not L1 // L3

      proof

        assume L1 // L3;

        then L1 = L3 by A2, A3, A5, A8, XBOOLE_0: 3, EUCLIDLP: 71;

        then

         A12: L2 // L4 by A7, A10, EUCLIDLP: 111, EUCLID12: 16;

        B in L2 & B in L4 by A6, A9, EUCLID_4: 41;

        then ( Line (A,B)) = ( Line (B,C)) by A6, A9, XBOOLE_0: 3, A12, EUCLIDLP: 71;

        then C in ( Line (A,B)) by EUCLID_4: 41;

        hence contradiction by A4, MENELAUS: 13, A1;

      end;

       not L1 is being_point & not L3 is being_point by A4, A5, A8, Th31, EUCLID12: 9;

      hence thesis by A5, A8, A11, EUCLID12: 21;

    end;

    theorem :: EUCLID13:66

    

     Th55: (A,B,C) is_a_triangle & |((C - A), (B - C))| = 0 implies (( the_altitude (A,B,C)) /\ ( the_altitude (B,C,A))) = {C} & (( the_altitude (B,C,A)) /\ ( the_altitude (C,A,B))) = {C} & (( the_altitude (C,A,B)) /\ ( the_altitude (A,B,C))) = {C}

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: |((C - A), (B - C))| = 0 ;

      

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

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

      then

       A4: not A in ( Line (B,C)) & not B in ( Line (C,A)) by A1, Th20;

      ( the_foot_of_the_altitude (A,B,C)) = C & ( the_foot_of_the_altitude (B,C,A)) = C by A1, A2, Th51;

      then ( the_altitude (A,B,C)) = ( Line (A,C)) & ( the_altitude (B,C,A)) = ( Line (B,C)) by A3, A4, Th36;

      then

       A5: C in ( the_altitude (A,B,C)) & C in ( the_altitude (B,C,A)) by EUCLID_4: 41;

      

       A6: C in ( the_altitude (C,A,B)) by A3, Th30;

      

       A7: (( the_altitude (A,B,C)) /\ ( the_altitude (B,C,A))) = {C}

      proof

        C in (( the_altitude (A,B,C)) /\ ( the_altitude (B,C,A))) by A5, XBOOLE_0:def 4;

        hence thesis by EUCLID12: 22, A1, A5, Th52;

      end;

      

       A8: (( the_altitude (B,C,A)) /\ ( the_altitude (C,A,B))) = {C}

      proof

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

        then

         A9: (( the_altitude (B,C,A)) /\ ( the_altitude (C,A,B))) is being_point by A5, A3, Th30, Th53;

        C in (( the_altitude (B,C,A)) /\ ( the_altitude (C,A,B))) by A5, A6, XBOOLE_0:def 4;

        hence thesis by A9, EUCLID12: 22;

      end;

      (( the_altitude (C,A,B)) /\ ( the_altitude (A,B,C))) = {C}

      proof

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

        then

         A10: (( the_altitude (C,A,B)) /\ ( the_altitude (A,B,C))) is being_point by A5, A3, Th30, Th54;

        C in (( the_altitude (C,A,B)) /\ ( the_altitude (A,B,C))) by A5, A6, XBOOLE_0:def 4;

        hence thesis by A10, EUCLID12: 22;

      end;

      hence thesis by A7, A8;

    end;

    theorem :: EUCLID13:67

    

     Th56: (A,B,C) is_a_triangle implies ex P be Point of ( TOP-REAL 2) st (( the_altitude (A,B,C)) /\ ( the_altitude (B,C,A))) = {P} & (( the_altitude (B,C,A)) /\ ( the_altitude (C,A,B))) = {P} & (( the_altitude (C,A,B)) /\ ( the_altitude (A,B,C))) = {P}

    proof

      assume

       A1: (A,B,C) is_a_triangle ;

      per cases ;

        suppose

         A2: |((C - A), (B - C))| = 0 ;

        take C;

        thus thesis by A1, A2, Th55;

      end;

        suppose

         A3: |((B - C), (A - B))| = 0 ;

        take B;

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

        hence thesis by A3, Th55;

      end;

        suppose

         A4: |((C - A), (A - B))| = 0 ;

        take A;

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

        hence thesis by A4, Th55;

      end;

        suppose not |((C - A), (B - C))| = 0 & not |((B - C), (A - B))| = 0 & not |((C - A), (A - B))| = 0 ;

        then

         A5: (( Line (A,( the_foot_of_the_altitude (A,B,C)))),( Line (C,( the_foot_of_the_altitude (C,A,B)))),( Line (B,( the_foot_of_the_altitude (B,C,A))))) are_concurrent by A1, Th50;

        

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

        

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

        then not A in ( Line (B,C)) & not B in ( Line (C,A)) & not C in ( Line (A,B)) by A1, Th20;

        then

         A8: ( the_altitude (A,B,C)) = ( Line (A,( the_foot_of_the_altitude (A,B,C)))) & ( the_altitude (C,A,B)) = ( Line (C,( the_foot_of_the_altitude (C,A,B)))) & ( the_altitude (B,C,A)) = ( Line (B,( the_foot_of_the_altitude (B,C,A)))) by A6, Th36;

        consider L1,L2 be Element of ( line_of_REAL 2) such that

         A9: ( the_altitude (A,B,C)) = L1 and

         A10: L2 = ( Line (B,C)) and A in L1 and

         A11: L1 _|_ L2 by A6, Def1;

        consider L3,L4 be Element of ( line_of_REAL 2) such that

         A12: ( the_altitude (C,A,B)) = L3 and

         A13: L4 = ( Line (A,B)) and C in L3 and

         A14: L3 _|_ L4 by A6, Def1;

        consider L5,L6 be Element of ( line_of_REAL 2) such that

         A15: ( the_altitude (B,C,A)) = L5 and

         A16: L6 = ( Line (C,A)) and B in L5 and

         A17: L5 _|_ L6 by A6, Def1;

        

         A18: not (( Line (A,( the_foot_of_the_altitude (A,B,C)))) is_parallel_to ( Line (C,( the_foot_of_the_altitude (C,A,B)))))

        proof

          assume

           A19: ( Line (A,( the_foot_of_the_altitude (A,B,C)))) is_parallel_to ( Line (C,( the_foot_of_the_altitude (C,A,B))));

          L1 is being_line & L3 is being_line & (L1,L3) are_coplane by A9, A12, A6, Th31, EUCLID12: 39;

          then L1 // L3 by A19, A8, A9, A12, EUCLIDLP: 113;

          then L1 _|_ L4 by A14, EUCLIDLP: 61;

          then

           A20: L2 // L4 by A11, EUCLIDLP: 111, EUCLID12: 16;

          B in L2 & B in L4 by A10, A13, EUCLID_4: 41;

          then ( Line (A,B)) = ( Line (B,C)) by A10, A13, A20, XBOOLE_0: 3, EUCLIDLP: 71;

          then C in ( Line (A,B)) by EUCLID_4: 41;

          hence contradiction by A7, A6, MENELAUS: 13;

        end;

        consider D such that

         A21: D in ( the_altitude (A,B,C)) and

         A22: D in ( the_altitude (C,A,B)) and

         A23: D in ( the_altitude (B,C,A)) by A8, A18, A5, MENELAUS:def 1;

        

         A24: D in (L1 /\ L3) & D in (L1 /\ L5) & D in (L3 /\ L5) by A21, A22, A23, A9, A12, A15, XBOOLE_0:def 4;

        

         A25: L1 meets L3 & L1 meets L5 & L3 meets L5 by A21, A22, A23, A9, A12, A15, XBOOLE_0:def 4;

        L1 <> L3

        proof

          assume L1 = L3;

          then

           A26: L2 // L4 by A14, A11, EUCLIDLP: 111, EUCLID12: 16;

          B in L2 & B in L4 by A10, A13, EUCLID_4: 41;

          then L2 = L4 by A26, XBOOLE_0: 3, EUCLIDLP: 71;

          then C in ( Line (A,B)) by A10, A13, EUCLID_4: 41;

          hence contradiction by A7, A6, MENELAUS: 13;

        end;

        then

         A27: not L1 // L3 by A25, EUCLIDLP: 71;

         not L1 is being_point & not L3 is being_point by A9, A12, A6, Th31, EUCLID12: 9;

        then

         A28: (L1 /\ L3) = {D} by A24, EUCLID12: 22, A27, EUCLID12: 21;

        L1 <> L5

        proof

          assume L1 = L5;

          then

           A29: L2 // L6 by A17, A11, EUCLIDLP: 111, EUCLID12: 16;

          C in L2 & C in L6 by A16, A10, EUCLID_4: 41;

          then L2 = L6 by A29, XBOOLE_0: 3, EUCLIDLP: 71;

          then A in ( Line (B,C)) by A16, A10, EUCLID_4: 41;

          hence contradiction by A1, A6, MENELAUS: 13;

        end;

        then

         A30: not L1 // L5 by A25, EUCLIDLP: 71;

         not L1 is being_point & not L5 is being_point by A15, A9, A6, Th31, EUCLID12: 9;

        then

         A31: (L1 /\ L5) = {D} by A24, EUCLID12: 22, A30, EUCLID12: 21;

        L3 <> L5

        proof

          assume L3 = L5;

          then

           A32: L4 // L6 by A17, A14, EUCLIDLP: 111, EUCLID12: 16;

          A in L4 & A in L6 by A16, A13, EUCLID_4: 41;

          then ( Line (A,B)) = ( Line (C,A)) by A16, A13, A32, XBOOLE_0: 3, EUCLIDLP: 71;

          then C in ( Line (A,B)) by EUCLID_4: 41;

          hence contradiction by A7, A6, MENELAUS: 13;

        end;

        then

         A33: not L3 // L5 by A25, EUCLIDLP: 71;

         not L3 is being_point & not L5 is being_point by A15, A12, A6, Th31, EUCLID12: 9;

        then (L3 /\ L5) = {D} by A24, EUCLID12: 22, A33, EUCLID12: 21;

        hence thesis by A28, A31, A9, A12, A15;

      end;

    end;

    definition

      let A,B,C be Point of ( TOP-REAL 2);

      assume

       A1: (A,B,C) is_a_triangle ;

      :: EUCLID13:def4

      func the_orthocenter (A,B,C) -> Point of ( TOP-REAL 2) means (( the_altitude (A,B,C)) /\ ( the_altitude (B,C,A))) = {it } & (( the_altitude (B,C,A)) /\ ( the_altitude (C,A,B))) = {it } & (( the_altitude (C,A,B)) /\ ( the_altitude (A,B,C))) = {it };

      existence by A1, Th56;

      uniqueness by ZFMISC_1: 3;

    end

    begin

    theorem :: EUCLID13:68

    

     Th57: B <> A implies ((( sin ( angle (B,A,C))) + ( sin ( angle (C,B,A)))) * ( |.(C - B).| - |.(C - A).|)) = ((( sin ( angle (B,A,C))) - ( sin ( angle (C,B,A)))) * ( |.(C - B).| + |.(C - A).|))

    proof

      assume B <> A;

      then ( |.(C - B).| * ( sin ( angle (C,B,A)))) = ( |.(C - A).| * ( sin ( angle (B,A,C)))) by EUCLID_6: 6;

      hence thesis;

    end;

    theorem :: EUCLID13:69

    

     Th58: B <> A implies ((( sin ((( angle (B,A,C)) + ( angle (C,B,A))) / 2)) * ( cos ((( angle (B,A,C)) - ( angle (C,B,A))) / 2))) * ( |.(C - B).| - |.(C - A).|)) = ((( sin ((( angle (B,A,C)) - ( angle (C,B,A))) / 2)) * ( cos ((( angle (B,A,C)) + ( angle (C,B,A))) / 2))) * ( |.(C - B).| + |.(C - A).|))

    proof

      assume B <> A;

      then

       A1: ((( sin ( angle (B,A,C))) + ( sin ( angle (C,B,A)))) * ( |.(C - B).| - |.(C - A).|)) = ((( sin ( angle (B,A,C))) - ( sin ( angle (C,B,A)))) * ( |.(C - B).| + |.(C - A).|)) by Th57;

      set BAC = ( angle (B,A,C)), CBA = ( angle (C,B,A));

      (( sin BAC) + ( sin CBA)) = (2 * (( cos ((BAC - CBA) / 2)) * ( sin ((BAC + CBA) / 2)))) by SIN_COS4: 15;

      then ((2 * (( cos ((BAC - CBA) / 2)) * ( sin ((BAC + CBA) / 2)))) * ( |.(C - B).| - |.(C - A).|)) = ((2 * (( cos ((BAC + CBA) / 2)) * ( sin ((BAC - CBA) / 2)))) * ( |.(C - B).| + |.(C - A).|)) by A1, SIN_COS4: 16;

      hence thesis;

    end;

    theorem :: EUCLID13:70

    

     Th59: (A,B,C) is_a_triangle & (( angle (B,A,C)) - ( angle (C,B,A))) <> PI & (( angle (B,A,C)) - ( angle (C,B,A))) <> ( - PI ) implies ( cos ((( angle (B,A,C)) - ( angle (C,B,A))) / 2)) <> 0

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: (( angle (B,A,C)) - ( angle (C,B,A))) <> PI and

       A3: (( angle (B,A,C)) - ( angle (C,B,A))) <> ( - PI );

      assume

       A4: ( cos ((( angle (B,A,C)) - ( angle (C,B,A))) / 2)) = 0 ;

      consider i0 be Integer such that

       A5: ((( angle (B,A,C)) - ( angle (C,B,A))) / 2) = (( PI / 2) + ( PI * i0)) by A4, BORSUK_7: 8;

      set a = (( angle (B,A,C)) - ( angle (C,B,A)));

      

       A6: 0 <= ( angle (B,A,C)) < (2 * PI ) & 0 <= ( angle (C,B,A)) < (2 * PI ) by EUCLID11: 2;

      then

       A7: 0 < ( angle (B,A,C)) < (2 * PI ) & 0 < ( angle (C,B,A)) < (2 * PI ) by A1, EUCLID10: 30;

      

       A8: ( 0 - (2 * PI )) < (( angle (B,A,C)) - ( angle (C,B,A))) by A7, XREAL_1: 14;

      (( angle (B,A,C)) - ( angle (C,B,A))) < ((2 * PI ) - 0 ) by A6, XREAL_1: 14;

      then ((( - 2) * PI ) / PI ) < (((1 + (2 * i0)) * PI ) / PI ) < ((2 * PI ) / PI ) & PI <> 0 by A8, A5, COMPTRIG: 5, XREAL_1: 74;

      then (( - 2) * ( PI / PI )) < ((1 + (2 * i0)) * ( PI / PI )) < (2 * ( PI / PI )) & ( PI / PI ) = 1 by XCMPLX_1: 60;

      then (( - 2) - 1) < ((1 + (2 * i0)) - 1) < (2 - 1) by XREAL_1: 14;

      then (( - 3) / 2) < ((2 * i0) / 2) < (1 / 2) by XREAL_1: 74;

      then i0 = 0 or i0 = ( - 1) by Th2;

      hence contradiction by A5, A2, A3;

    end;

    theorem :: EUCLID13:71

    

     Th60: (A,C,B) is_a_triangle & ( angle (A,C,B)) < PI implies ( tan ((( angle (B,A,C)) - ( angle (C,B,A))) / 2)) = (( cot (( angle (A,C,B)) / 2)) * (( |.(C - B).| - |.(C - A).|) / ( |.(C - B).| + |.(C - A).|)))

    proof

      assume that

       A1: (A,C,B) is_a_triangle and

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

      

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

      

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

      then

       A5: ((( angle (B,A,C)) - ( angle (C,B,A))) <> PI & (( angle (B,A,C)) - ( angle (C,B,A))) <> ( - PI )) by Th25, Th26;

      set alpha = ((( angle (B,A,C)) - ( angle (C,B,A))) / 2), beta = ((( angle (B,A,C)) + ( angle (C,B,A))) / 2);

      ( angle (A,C,B)) = ( PI - (( angle (C,B,A)) + ( angle (B,A,C)))) by A1, A2, Th23;

      then

       A8: beta = (( PI / 2) - (( angle (A,C,B)) / 2));

      set a2 = (( angle (A,C,B)) / 2);

      

       A9: ( sin beta) = ( cos a2) & ( cos beta) = ( sin a2) by A8, SIN_COS: 79;

      

       A10: ( sin a2) <> 0 by A1, Th21;

      

       A11: ( |.(C - B).| + |.(C - A).|) <> 0

      proof

         |.(C - B).| <> 0 & |.(C - A).| <> 0 by A3, EUCLID_6: 42;

        hence thesis;

      end;

      ((( sin beta) * ( cos alpha)) * ( |.(C - B).| - |.(C - A).|)) = ((( sin alpha) * ( cos beta)) * ( |.(C - B).| + |.(C - A).|)) by A3, Th58;

      then (((( |.(C - B).| - |.(C - A).|) * ( cos a2)) * ( cos alpha)) / ( cos alpha)) = (((( |.(C - B).| + |.(C - A).|) * ( sin a2)) * ( sin alpha)) / ( cos alpha)) by A9;

      then ((( |.(C - B).| - |.(C - A).|) * ( cos a2)) * (( cos alpha) / ( cos alpha))) = ((( |.(C - B).| + |.(C - A).|) * ( sin a2)) * (( sin alpha) / ( cos alpha)));

      then ((( |.(C - B).| - |.(C - A).|) * ( cos a2)) * 1) = ((( |.(C - B).| + |.(C - A).|) * ( sin a2)) * (( sin alpha) / ( cos alpha))) by A5, A4, Th59, XCMPLX_1: 60;

      then ((( |.(C - B).| - |.(C - A).|) * ( cos a2)) / ( sin a2)) = (((( |.(C - B).| + |.(C - A).|) * ( tan alpha)) * ( sin a2)) / ( sin a2));

      

      then (( |.(C - B).| - |.(C - A).|) * (( cos a2) / ( sin a2))) = ((( |.(C - B).| + |.(C - A).|) * ( tan alpha)) * (( sin a2) / ( sin a2)))

      .= ((( |.(C - B).| + |.(C - A).|) * ( tan alpha)) * 1) by A10, XCMPLX_1: 60;

      then ((( tan alpha) * ( |.(C - B).| + |.(C - A).|)) / ( |.(C - B).| + |.(C - A).|)) = ((( cot a2) * ( |.(C - B).| - |.(C - A).|)) / ( |.(C - B).| + |.(C - A).|));

      then (( tan alpha) * (( |.(C - B).| + |.(C - A).|) / ( |.(C - B).| + |.(C - A).|))) = (( cot a2) * (( |.(C - B).| - |.(C - A).|) / ( |.(C - B).| + |.(C - A).|)));

      then (( tan alpha) * 1) = (( cot a2) * (( |.(C - B).| - |.(C - A).|) / ( |.(C - B).| + |.(C - A).|))) by A11, XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: EUCLID13:72

    

     Th61: (A,C,B) is_a_triangle & ( angle (A,C,B)) < PI implies ((( angle (B,A,C)) - ( angle (C,B,A))) / 2) = ( arctan (( cot (( angle (A,C,B)) / 2)) * (( |.(C - B).| - |.(C - A).|) / ( |.(C - B).| + |.(C - A).|))))

    proof

      assume that

       A1: (A,C,B) is_a_triangle and

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

      set r = ((( angle (B,A,C)) - ( angle (C,B,A))) / 2);

      

       A3: ( tan r) = (( cot (( angle (A,C,B)) / 2)) * (( |.(C - B).| - |.(C - A).|) / ( |.(C - B).| + |.(C - A).|))) by A1, A2, Th60;

       0 <= ( angle (A,C,B)) by EUCLID11: 2;

      then

       A4: 0 < ( angle (A,C,B)) < PI & (A,C,B) are_mutually_distinct by A1, A2, EUCLID10: 30, EUCLID_6: 20;

       0 < ( angle (B,A,C)) < PI & (A,B,C) is_a_triangle by A4, EUCLID11: 5, A1, MENELAUS: 15;

      then ( - ( PI / 2)) < r < ( PI / 2) by Th29;

      hence thesis by A3, SIN_COS9: 35;

    end;

    theorem :: EUCLID13:73

    

     Th62: (A,C,B) is_a_triangle & ( angle (A,C,B)) < PI implies (( angle (B,A,C)) - ( angle (C,B,A))) = (2 * ( arctan (( cot (( angle (A,C,B)) / 2)) * (( |.(C - B).| - |.(C - A).|) / ( |.(C - B).| + |.(C - A).|)))))

    proof

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

      then ((( angle (B,A,C)) - ( angle (C,B,A))) / 2) = ( arctan (( cot (( angle (A,C,B)) / 2)) * (( |.(C - B).| - |.(C - A).|) / ( |.(C - B).| + |.(C - A).|)))) by Th61;

      hence thesis;

    end;

    theorem :: EUCLID13:74

    (A,C,B) is_a_triangle & ( angle (A,C,B)) < PI implies ( angle (B,A,C)) = ((( arctan (( cot (( angle (A,C,B)) / 2)) * (( |.(C - B).| - |.(C - A).|) / ( |.(C - B).| + |.(C - A).|)))) + ( PI / 2)) - (( angle (A,C,B)) / 2)) & ( angle (C,B,A)) = ((( PI / 2) - (( angle (A,C,B)) / 2)) - ( arctan (( cot (( angle (A,C,B)) / 2)) * (( |.(C - B).| - |.(C - A).|) / ( |.(C - B).| + |.(C - A).|)))))

    proof

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

      then (( angle (B,A,C)) - ( angle (C,B,A))) = (2 * ( arctan (( cot (( angle (A,C,B)) / 2)) * (( |.(C - B).| - |.(C - A).|) / ( |.(C - B).| + |.(C - A).|))))) & (( angle (B,A,C)) + ( angle (C,B,A))) = ( PI - ( angle (A,C,B))) by Th62, Th24;

      hence thesis;

    end;

    theorem :: EUCLID13:75

    

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

    proof

      assume that

       A1: (A,C,B) is_a_triangle and

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

      

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

      

       A4: |.(B - C).| = (( |.(A - B).| * ( sin ( angle (B,A,C)))) / ( sin ( angle (A,C,B))))

      proof

        ( |.(B - A).| * ( sin ( angle (B,A,C)))) = ( |.(B - C).| * ( sin ( angle (A,C,B)))) by A3, EUCLID_6: 6;

        

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

        .= ( |.(B - C).| * (( sin ( angle (A,C,B))) / ( sin ( angle (A,C,B)))))

        .= ( |.(B - C).| * 1) by A1, Th22, XCMPLX_1: 60

        .= |.(B - C).|;

        hence thesis;

      end;

      ( angle (A,C,B)) = ( PI - (( angle (C,B,A)) + ( angle (B,A,C)))) by A1, A2, Th23;

      hence thesis by A4, EUCLID10: 1;

    end;

    theorem :: EUCLID13:76

    

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

    proof

      assume that

       A1: (A,C,B) is_a_triangle and

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

      

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

      

       A4: |.(A - C).| = (( |.(A - B).| * ( sin ( angle (C,B,A)))) / ( sin ( angle (A,C,B))))

      proof

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

        .= ( |.(A - C).| * (( sin ( angle (A,C,B))) / ( sin ( angle (A,C,B)))))

        .= ( |.(A - C).| * 1) by A1, Th22, XCMPLX_1: 60

        .= |.(A - C).|;

        hence thesis;

      end;

      ( angle (A,C,B)) = ( PI - (( angle (C,B,A)) + ( angle (B,A,C))))

      proof

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

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

        hence thesis;

      end;

      hence thesis by A4, EUCLID10: 1;

    end;

    theorem :: EUCLID13:77

    

     Th65: (A,C,B) is_a_triangle & ( angle (C,A,B)) = ( PI / 2) implies ( the_length_of_the_altitude (C,A,B)) = ( |.(A - B).| * ( tan ( angle (A,B,C))))

    proof

      assume that

       A1: (A,C,B) is_a_triangle and

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

      

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

      then |((B - A), (C - A))| = 0 by A2, EUCLID_3: 45;

      then

       A4: |((A - B), (A - C))| = 0 by Th10;

      (( tan ( angle (A,B,C))) * |.(A - B).|) = (( |.(A - C).| / |.(A - B).|) * |.(A - B).|) by A1, A2, EUCLID10: 35

      .= |.(A - C).| by A3, EUCLID_6: 42, XCMPLX_1: 87

      .= |.(C - A).| by EUCLID_6: 43;

      

      then (( tan ( angle (A,B,C))) * |.(A - B).|) = |.(( the_foot_of_the_altitude (C,A,B)) - C).| by A4, A3, Th47

      .= |.(C - ( the_foot_of_the_altitude (C,A,B))).| by EUCLID_6: 43;

      hence thesis by A3, Def3;

    end;

    theorem :: EUCLID13:78

    

     Th66: (A,B,C) is_a_triangle & ( angle (C,A,B)) = ((3 / 2) * PI ) implies ( the_length_of_the_altitude (C,A,B)) = ( |.(A - B).| * ( tan ( angle (C,B,A))))

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: ( angle (C,A,B)) = ((3 / 2) * PI );

      

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

      then |((C - A), (B - A))| = 0 by A2, EUCLID_3: 45;

      then

       A4: |((A - B), (A - C))| = 0 by Th10;

      ( angle (B,A,C)) = ((2 * PI ) - ((3 / 2) * PI )) by A1, A2, EUCLID10: 31

      .= ( PI / 2);

      

      then (( tan ( angle (C,B,A))) * |.(A - B).|) = (( |.(A - C).| / |.(A - B).|) * |.(A - B).|) by A1, EUCLID10: 35

      .= |.(A - C).| by A3, EUCLID_6: 42, XCMPLX_1: 87

      .= |.(C - A).| by EUCLID_6: 43;

      

      then ( |.(A - B).| * ( tan ( angle (C,B,A)))) = |.(( the_foot_of_the_altitude (C,A,B)) - C).| by A4, A3, Th47

      .= |.(C - ( the_foot_of_the_altitude (C,A,B))).| by EUCLID_6: 43;

      hence thesis by A3, Def3;

    end;

    theorem :: EUCLID13:79

    (A,C,B) is_a_triangle & |((A - C), (A - B))| = 0 implies ( the_length_of_the_altitude (C,A,B)) = ( |.(A - B).| * |.( tan ( angle (A,B,C))).|)

    proof

      assume that

       A1: (A,C,B) is_a_triangle and

       A2: |((A - C), (A - B))| = 0 ;

      

       A3: (A,C,B) are_mutually_distinct & |((C - A), (B - A))| = 0 by A2, Th10, A1, EUCLID_6: 20;

      

       A4: |.(A - B).| <> 0 by A3, EUCLID_6: 42;

      per cases by A3, EUCLID_3: 45;

        suppose ( angle (C,A,B)) = ( PI / 2);

        then

         A5: ( the_length_of_the_altitude (C,A,B)) = ( |.(A - B).| * ( tan ( angle (A,B,C)))) by A1, Th65;

        then 0 <= ( tan ( angle (A,B,C))) by A4, A3, Th46;

        hence thesis by A5, ABSVALUE:def 1;

      end;

        suppose

         A6: ( angle (C,A,B)) = ((3 / 2) * PI );

        

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

        ( tan ( angle (C,B,A))) = ( tan ((2 * PI ) - ( angle (A,B,C)))) by A1, EUCLID10: 31

        .= ( - ( tan ( angle (A,B,C)))) by Th6;

        then

         A8: (( - ( tan ( angle (A,B,C)))) * |.(A - B).|) = ( the_length_of_the_altitude (C,A,B)) by A7, A6, Th66;

        then ( tan ( angle (A,B,C))) <= 0 by A4, A3, Th46;

        hence thesis by A8, ABSVALUE: 30;

      end;

    end;

    theorem :: EUCLID13:80

    

     Th67: B <> C & (( the_foot_of_the_altitude (A,B,C)),B,A) is_a_triangle implies ( |.(A - B).| * ( sin ( angle (A,B,( the_foot_of_the_altitude (A,B,C)))))) = |.(( the_foot_of_the_altitude (A,B,C)) - A).| or ( |.(A - B).| * ( - ( sin ( angle (A,B,( the_foot_of_the_altitude (A,B,C))))))) = |.(( the_foot_of_the_altitude (A,B,C)) - A).|

    proof

      assume that

       A1: B <> C and

       A2: (( the_foot_of_the_altitude (A,B,C)),B,A) is_a_triangle ;

       |((B - ( the_foot_of_the_altitude (A,B,C))), (A - ( the_foot_of_the_altitude (A,B,C))))| = 0 by A1, Th39;

      hence thesis by A2, EUCLID10: 32;

    end;

    theorem :: EUCLID13:81

    (A,B,C) is_a_triangle & |((B - A), (B - C))| <> 0 implies ( |.(A - B).| * ( sin ( angle (A,B,( the_foot_of_the_altitude (A,B,C)))))) = |.(( the_foot_of_the_altitude (A,B,C)) - A).| or ( |.(A - B).| * ( - ( sin ( angle (A,B,( the_foot_of_the_altitude (A,B,C))))))) = |.(( the_foot_of_the_altitude (A,B,C)) - A).|

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: |((B - A), (B - C))| <> 0 ;

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

      hence thesis by A1, A2, Th67, Th45;

    end;

    theorem :: EUCLID13:82

    (A,C,B) is_a_triangle & ( angle (A,C,B)) < PI & |((A - C), (A - B))| <> 0 implies ( the_length_of_the_altitude (C,A,B)) = ( |.(A - B).| * |.((( sin ( angle (C,B,A))) / ( sin (( angle (B,A,C)) + ( angle (C,B,A))))) * ( sin ( angle (C,A,( the_foot_of_the_altitude (C,A,B)))))).|)

    proof

      assume that

       A1: (A,C,B) is_a_triangle and

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

       A3: |((A - C), (A - B))| <> 0 ;

      

       A4: |.(A - C).| = (( |.(A - B).| * ( sin ( angle (C,B,A)))) / ( sin (( angle (B,A,C)) + ( angle (C,B,A))))) by A1, A2, Th64;

      

       A5: (C,A,B) is_a_triangle & (A,C,B) are_mutually_distinct by A1, EUCLID_6: 20, MENELAUS: 15;

      then |.(( the_foot_of_the_altitude (C,A,B)) - C).| = ( |.(C - A).| * ( sin ( angle (C,A,( the_foot_of_the_altitude (C,A,B)))))) or |.(( the_foot_of_the_altitude (C,A,B)) - C).| = ( |.(C - A).| * ( - ( sin ( angle (C,A,( the_foot_of_the_altitude (C,A,B))))))) by A3, Th45, Th67;

      then |.(( the_foot_of_the_altitude (C,A,B)) - C).| = ( |.(A - C).| * ( sin ( angle (C,A,( the_foot_of_the_altitude (C,A,B)))))) or |.(( the_foot_of_the_altitude (C,A,B)) - C).| = ( |.(A - C).| * ( - ( sin ( angle (C,A,( the_foot_of_the_altitude (C,A,B))))))) by EUCLID_6: 43;

      per cases by A4;

        suppose

         A7: |.(( the_foot_of_the_altitude (C,A,B)) - C).| = ( |.(A - B).| * ((( sin ( angle (C,B,A))) / ( sin (( angle (B,A,C)) + ( angle (C,B,A))))) * ( sin ( angle (C,A,( the_foot_of_the_altitude (C,A,B)))))));

         |.(A - B).| <> 0 by A5, EUCLID_6: 42;

        then

         A8: 0 <= ((( sin ( angle (C,B,A))) / ( sin (( angle (B,A,C)) + ( angle (C,B,A))))) * ( sin ( angle (C,A,( the_foot_of_the_altitude (C,A,B)))))) by A7;

        ( the_length_of_the_altitude (C,A,B)) = |.(C - ( the_foot_of_the_altitude (C,A,B))).| by A5, Def3

        .= |.(( the_foot_of_the_altitude (C,A,B)) - C).| by EUCLID_6: 43

        .= ( |.(A - B).| * |.((( sin ( angle (C,B,A))) / ( sin (( angle (B,A,C)) + ( angle (C,B,A))))) * ( sin ( angle (C,A,( the_foot_of_the_altitude (C,A,B)))))).|) by A7, A8, ABSVALUE:def 1;

        hence thesis;

      end;

        suppose

         A10: |.(( the_foot_of_the_altitude (C,A,B)) - C).| = ( |.(A - B).| * ( - ((( sin ( angle (C,B,A))) / ( sin (( angle (B,A,C)) + ( angle (C,B,A))))) * ( sin ( angle (C,A,( the_foot_of_the_altitude (C,A,B))))))));

         |.(A - B).| <> 0 by A5, EUCLID_6: 42;

        then

         A11: ((( sin ( angle (C,B,A))) / ( sin (( angle (B,A,C)) + ( angle (C,B,A))))) * ( sin ( angle (C,A,( the_foot_of_the_altitude (C,A,B)))))) <= 0 by A10;

        ( the_length_of_the_altitude (C,A,B)) = |.(C - ( the_foot_of_the_altitude (C,A,B))).| by A5, Def3

        .= |.(( the_foot_of_the_altitude (C,A,B)) - C).| by EUCLID_6: 43

        .= ( |.(A - B).| * |.((( sin ( angle (C,B,A))) / ( sin (( angle (B,A,C)) + ( angle (C,B,A))))) * ( sin ( angle (C,A,( the_foot_of_the_altitude (C,A,B)))))).|) by A10, A11, ABSVALUE: 30;

        hence thesis;

      end;

    end;

    theorem :: EUCLID13:83

     0 < ( angle (B,A,D)) < PI & 0 < ( angle (D,A,C)) < PI & (D,A,C) are_mutually_distinct & (B,A,D) are_mutually_distinct implies (( angle (A,C,D)) + ( angle (D,B,A))) = ((2 * PI ) - ((( angle (B,A,C)) + ( angle (A,D,B))) + ( angle (C,D,A))))

    proof

      assume that

       A1: 0 < ( angle (B,A,D)) < PI and

       A2: 0 < ( angle (D,A,C)) < PI and

       A3: (D,A,C) are_mutually_distinct and

       A4: (B,A,D) are_mutually_distinct ;

      

       A5: (( angle (B,A,D)) + ( angle (D,A,C))) = ( angle (B,A,C))

      proof

         not (( angle (B,A,D)) + ( angle (D,A,C))) = (( angle (B,A,C)) + (2 * PI ))

        proof

          assume

           A6: (( angle (B,A,D)) + ( angle (D,A,C))) = (( angle (B,A,C)) + (2 * PI ));

           0 <= ( angle (B,A,C)) by EUCLID11: 2;

          then

           A7: ( 0 + (2 * PI )) <= (( angle (B,A,C)) + (2 * PI )) by XREAL_1: 7;

          (( angle (B,A,D)) + ( angle (D,A,C))) < ( PI + PI ) by A1, A2, XREAL_1: 8;

          hence contradiction by A7, A6;

        end;

        hence thesis by EUCLID_6: 4;

      end;

      

       A8: ( angle (A,C,D)) = ( PI - (( angle (C,D,A)) + ( angle (D,A,C))))

      proof

        ((( angle (D,A,C)) + ( angle (A,C,D))) + ( angle (C,D,A))) = PI by A2, A3, EUCLID_3: 47;

        hence thesis;

      end;

      ( angle (D,B,A)) = ( PI - (( angle (A,D,B)) + ( angle (B,A,D))))

      proof

        ((( angle (B,A,D)) + ( angle (A,D,B))) + ( angle (D,B,A))) = PI by A1, A4, EUCLID_3: 47;

        hence thesis;

      end;

      hence thesis by A8, A5;

    end;

    theorem :: EUCLID13:84

    

     Th68: (A,C,B) is_a_triangle & ( angle (A,C,B)) < PI & (A,D,B) is_a_triangle & ( angle (A,D,B)) < PI & a = ( angle (C,B,A)) & b = ( angle (B,A,C)) & c = ( angle (D,B,A)) & d = ( angle (C,A,D)) implies ( |.(D - C).| ^2 ) = (( |.(A - B).| ^2 ) * ((((( sin a) / ( sin (a + b))) ^2 ) + ((( sin c) / ( sin ((b + d) + c))) ^2 )) - (((2 * (( sin a) / ( sin (b + a)))) * (( sin c) / ( sin ((b + d) + c)))) * ( cos d))))

    proof

      assume that

       A1: (A,C,B) is_a_triangle and

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

       A3: (A,D,B) is_a_triangle and

       A4: ( angle (A,D,B)) < PI and

       A5: a = ( angle (C,B,A)) & b = ( angle (B,A,C)) & c = ( angle (D,B,A)) & d = ( angle (C,A,D));

      set e = (b + d);

      

       A6: e = ( angle (B,A,D)) or e = (( angle (B,A,D)) + (2 * PI )) by A5, EUCLID_6: 4;

      

       A7: ( sin (e + c)) = ( sin (( angle (B,A,D)) + ( angle (D,B,A))))

      proof

        ( sin ((( angle (B,A,D)) + c) + (2 * PI ))) = ( sin (( angle (B,A,D)) + c)) by SIN_COS: 79;

        hence thesis by A5, A6;

      end;

      

       A8: |.(C - A).| = |.(A - C).| by EUCLID_6: 43

      .= (( |.(A - B).| * ( sin ( angle (C,B,A)))) / ( sin (( angle (B,A,C)) + ( angle (C,B,A))))) by A1, A2, Th64;

      

      then

       A9: ( |.(C - A).| ^2 ) = (( |.(A - B).| * (( sin ( angle (C,B,A))) / ( sin (( angle (B,A,C)) + ( angle (C,B,A)))))) ^2 )

      .= (( |.(A - B).| ^2 ) * ((( sin ( angle (C,B,A))) / ( sin (( angle (B,A,C)) + ( angle (C,B,A))))) ^2 )) by SQUARE_1: 9;

      

       A10: |.(D - A).| = |.(A - D).| by EUCLID_6: 43

      .= (( |.(A - B).| * ( sin ( angle (D,B,A)))) / ( sin (( angle (B,A,D)) + ( angle (D,B,A))))) by A3, A4, Th64;

      

      then

       A11: ( |.(D - A).| ^2 ) = (( |.(A - B).| * (( sin ( angle (D,B,A))) / ( sin (( angle (B,A,D)) + ( angle (D,B,A)))))) ^2 )

      .= (( |.(A - B).| ^2 ) * ((( sin ( angle (D,B,A))) / ( sin (( angle (B,A,D)) + ( angle (D,B,A))))) ^2 )) by SQUARE_1: 9;

      ( |.(D - C).| ^2 ) = (((( |.(A - B).| ^2 ) * ((( sin ( angle (C,B,A))) / ( sin (( angle (B,A,C)) + ( angle (C,B,A))))) ^2 )) + (( |.(A - B).| ^2 ) * ((( sin ( angle (D,B,A))) / ( sin (( angle (B,A,D)) + ( angle (D,B,A))))) ^2 ))) - (((2 * (( |.(A - B).| * ( sin ( angle (C,B,A)))) / ( sin (( angle (B,A,C)) + ( angle (C,B,A)))))) * (( |.(A - B).| * ( sin ( angle (D,B,A)))) / ( sin (( angle (B,A,D)) + ( angle (D,B,A)))))) * ( cos ( angle (C,A,D))))) by A8, A9, A10, A11, EUCLID_6: 7

      .= (((( |.(A - B).| ^2 ) * ((( sin ( angle (C,B,A))) / ( sin (( angle (B,A,C)) + ( angle (C,B,A))))) ^2 )) + (( |.(A - B).| ^2 ) * ((( sin ( angle (D,B,A))) / ( sin (( angle (B,A,D)) + ( angle (D,B,A))))) ^2 ))) - ((((2 * ((( |.(A - B).| * |.(A - B).|) * ( sin ( angle (C,B,A)))) / ( sin (( angle (B,A,C)) + ( angle (C,B,A)))))) * ( sin ( angle (D,B,A)))) / ( sin (( angle (B,A,D)) + ( angle (D,B,A))))) * ( cos ( angle (C,A,D)))))

      .= (((( |.(A - B).| ^2 ) * ((( sin ( angle (C,B,A))) / ( sin (( angle (B,A,C)) + ( angle (C,B,A))))) ^2 )) + (( |.(A - B).| ^2 ) * ((( sin ( angle (D,B,A))) / ( sin (( angle (B,A,D)) + ( angle (D,B,A))))) ^2 ))) - ((((2 * ((( |.(A - B).| ^2 ) * ( sin ( angle (C,B,A)))) / ( sin (( angle (B,A,C)) + ( angle (C,B,A)))))) * ( sin ( angle (D,B,A)))) / ( sin (( angle (B,A,D)) + ( angle (D,B,A))))) * ( cos ( angle (C,A,D))))) by SQUARE_1:def 1

      .= (( |.(A - B).| ^2 ) * ((((( sin a) / ( sin (a + b))) ^2 ) + ((( sin c) / ( sin (e + c))) ^2 )) - (((2 * (( sin a) / ( sin (b + a)))) * (( sin c) / ( sin (e + c)))) * ( cos d)))) by A5, A7;

      hence thesis;

    end;

    theorem :: EUCLID13:85

    

     Th69: (( sin (2 * s)) * ( cos d)) = ( cos (2 * t)) implies ((((r * ( cos s)) ^2 ) + ((r * ( sin s)) ^2 )) - (((2 * (r * ( cos s))) * (r * ( sin s))) * ( cos d))) = ((2 * (r ^2 )) * (( sin t) ^2 ))

    proof

      assume

       A1: (( sin (2 * s)) * ( cos d)) = ( cos (2 * t));

      ((((r * ( cos s)) ^2 ) + ((r * ( sin s)) ^2 )) - (((2 * (r * ( cos s))) * (r * ( sin s))) * ( cos d))) = ((((r * ( cos s)) * (r * ( cos s))) + ((r * ( sin s)) ^2 )) - (((2 * (r * ( cos s))) * (r * ( sin s))) * ( cos d))) by SQUARE_1:def 1

      .= ((((r * ( cos s)) * (r * ( cos s))) + ((r * ( sin s)) * (r * ( sin s)))) - (((2 * (r * ( cos s))) * (r * ( sin s))) * ( cos d))) by SQUARE_1:def 1

      .= (((r * r) * ((( cos s) * ( cos s)) + (( sin s) * ( sin s)))) - (((((r * 2) * r) * ( cos s)) * ( sin s)) * ( cos d)))

      .= (((r * r) * 1) - (((((r * 2) * r) * ( cos s)) * ( sin s)) * ( cos d))) by SIN_COS: 29

      .= ((r ^2 ) - (((((r * r) * 2) * ( cos s)) * ( sin s)) * ( cos d))) by SQUARE_1:def 1

      .= ((r ^2 ) - (((((r ^2 ) * 2) * ( cos s)) * ( sin s)) * ( cos d))) by SQUARE_1:def 1

      .= ((r ^2 ) - (((r ^2 ) * ((2 * ( sin s)) * ( cos s))) * ( cos d)))

      .= ((r ^2 ) - (((r ^2 ) * ( sin (2 * s))) * ( cos d))) by SIN_COS5: 5

      .= ((r ^2 ) - ((r ^2 ) * ( cos (2 * t)))) by A1

      .= ((r ^2 ) - ((r ^2 ) * ((( cos t) ^2 ) - (( sin t) ^2 )))) by SIN_COS5: 7

      .= ((r ^2 ) * (1 - ((( cos t) ^2 ) - (( sin t) ^2 ))))

      .= ((r ^2 ) * (((( cos t) ^2 ) + (( sin t) ^2 )) - ((( cos t) ^2 ) - (( sin t) ^2 )))) by SIN_COS: 29

      .= ((2 * (r ^2 )) * (( sin t) ^2 ));

      hence thesis;

    end;

    theorem :: EUCLID13:86

    for R,theta be Real st D <> C & 0 <= R & (A,C,B) is_a_triangle & ( angle (A,C,B)) < PI & (A,D,B) is_a_triangle & ( angle (A,D,B)) < PI & a = ( angle (C,B,A)) & b = ( angle (B,A,C)) & c = ( angle (D,B,A)) & d = ( angle (C,A,D)) & (R * ( cos s)) = (( sin a) / ( sin (a + b))) & (R * ( sin s)) = (( sin c) / ( sin ((b + d) + c))) & 0 < theta < PI & (( sin (2 * s)) * ( cos d)) = ( cos (2 * theta)) holds |.(D - C).| = ((( |.(A - B).| * ( sqrt 2)) * R) * ( sin theta))

    proof

      let R,theta be Real;

      assume that

       A1: D <> C and

       A2: 0 <= R and

       A3: (A,C,B) is_a_triangle & ( angle (A,C,B)) < PI & (A,D,B) is_a_triangle & ( angle (A,D,B)) < PI & a = ( angle (C,B,A)) & b = ( angle (B,A,C)) & c = ( angle (D,B,A)) & d = ( angle (C,A,D)) and

       A4: (R * ( cos s)) = (( sin a) / ( sin (a + b))) and

       A5: (R * ( sin s)) = (( sin c) / ( sin ((b + d) + c))) and

       A6: 0 < theta < PI and

       A7: (( sin (2 * s)) * ( cos d)) = ( cos (2 * theta));

      

       A8: ( |.(D - C).| ^2 ) = (( |.(A - B).| ^2 ) * ((((R * ( cos s)) ^2 ) + ((R * ( sin s)) ^2 )) - (((2 * (R * ( cos s))) * (R * ( sin s))) * ( cos d)))) by A3, A4, A5, Th68

      .= (( |.(A - B).| ^2 ) * ((2 * (R ^2 )) * (( sin theta) ^2 ))) by A7, Th69;

      

       A9: 0 < 2 & ( sqrt (2 * 2)) = 2 by SQUARE_1: 20;

      

       A10: (( |.(A - B).| ^2 ) * ((2 * (R ^2 )) * (( sin theta) ^2 ))) = (( |.(A - B).| * |.(A - B).|) * ((2 * (R ^2 )) * (( sin theta) ^2 ))) by SQUARE_1:def 1

      .= (( |.(A - B).| * |.(A - B).|) * (((( sqrt 2) * ( sqrt 2)) * (R ^2 )) * (( sin theta) ^2 ))) by A9, SQUARE_1: 29

      .= (( |.(A - B).| * |.(A - B).|) * (((( sqrt 2) * ( sqrt 2)) * (R * R)) * (( sin theta) ^2 ))) by SQUARE_1:def 1

      .= (( |.(A - B).| * |.(A - B).|) * (((( sqrt 2) * ( sqrt 2)) * (R * R)) * (( sin theta) * ( sin theta)))) by SQUARE_1:def 1

      .= (((( |.(A - B).| * ( sqrt 2)) * R) * ( sin theta)) * ((( |.(A - B).| * ( sqrt 2)) * R) * ( sin theta)))

      .= (((( |.(A - B).| * ( sqrt 2)) * R) * ( sin theta)) ^2 ) by SQUARE_1:def 1;

      ((2 * PI ) * 0 ) < theta < (((2 * PI ) * 0 ) + PI ) by A6;

      then

       A11: 0 < ( sin theta) by SIN_COS6: 11;

       not |.(D - C).| = ( - ((( |.(A - B).| * ( sqrt 2)) * R) * ( sin theta)))

      proof

        assume

         A12: |.(D - C).| = ( - ((( |.(A - B).| * ( sqrt 2)) * R) * ( sin theta)));

         0 < ( sqrt 2) by SQUARE_1: 25;

        then |.(D - C).| = 0 by A12, A2, A11;

        hence contradiction by A1, EUCLID_6: 42;

      end;

      hence thesis by A10, A8, SQUARE_1: 40;

    end;

    theorem :: EUCLID13:87

    

     Th70: (A,C,B) is_a_triangle & ( angle (A,C,B)) < PI & (D,A,C) is_a_triangle & ( angle (A,D,C)) = ( PI / 2) implies |.(D - C).| = ((( |.(A - B).| * ( sin ( angle (C,B,A)))) / ( sin (( angle (B,A,C)) + ( angle (C,B,A))))) * ( sin ( angle (C,A,D))))

    proof

      assume that

       A1: (A,C,B) is_a_triangle and

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

       A3: (D,A,C) is_a_triangle and

       A4: ( angle (A,D,C)) = ( PI / 2);

       |.(D - C).| = ( |.(C - A).| * ( sin ( angle (C,A,D)))) by A3, A4, EUCLID10: 34

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

      .= ((( |.(A - B).| * ( sin ( angle (C,B,A)))) / ( sin (( angle (B,A,C)) + ( angle (C,B,A))))) * ( sin ( angle (C,A,D)))) by A1, A2, Th64;

      hence thesis;

    end;

    theorem :: EUCLID13:88

    

     Th71: (B,C,A) is_a_triangle & ( angle (B,C,A)) < PI & (D,C,A) is_a_triangle & ( angle (C,D,A)) = ( PI / 2) implies |.(D - C).| = ((( |.(A - B).| * ( sin ( angle (A,B,C)))) / ( sin (( angle (A,B,C)) + ( angle (C,A,B))))) * ( sin ( angle (D,A,C))))

    proof

      assume that

       A1: (B,C,A) is_a_triangle and

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

       A3: (D,C,A) is_a_triangle and

       A4: ( angle (C,D,A)) = ( PI / 2);

       |.(D - C).| = ( |.(A - C).| * ( sin ( angle (D,A,C)))) by A3, A4, EUCLID10: 34

      .= ((( |.(B - A).| * ( sin ( angle (A,B,C)))) / ( sin (( angle (A,B,C)) + ( angle (C,A,B))))) * ( sin ( angle (D,A,C)))) by A1, A2, Th63;

      hence thesis by EUCLID_6: 43;

    end;

    theorem :: EUCLID13:89

    (A,C,B) is_a_triangle & ( angle (A,C,B)) < PI & (D,A,C) is_a_triangle & ( angle (A,D,C)) = ( PI / 2) & A in ( LSeg (B,D)) & A <> D implies |.(D - C).| = ((( |.(A - B).| * ( sin ( angle (C,B,A)))) / ( sin (( angle (C,A,D)) - ( angle (C,B,A))))) * ( sin ( angle (C,A,D))))

    proof

      assume that

       A1: (A,C,B) is_a_triangle and

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

       A3: (D,A,C) is_a_triangle and

       A4: ( angle (A,D,C)) = ( PI / 2) and

       A5: A in ( LSeg (B,D)) and

       A6: A <> D;

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

      then (( angle (B,A,C)) + ( angle (C,A,D))) = PI or (( angle (B,A,C)) + ( angle (C,A,D))) = (3 * PI ) by A5, A6, EUCLID_6: 13;

      then ( sin (( angle (B,A,C)) + ( angle (C,B,A)))) = ( sin ( PI - (( angle (C,A,D)) - ( angle (C,B,A))))) or ( sin (( angle (B,A,C)) + ( angle (C,B,A)))) = ( sin (((2 * PI ) * 1) + ( PI - (( angle (C,A,D)) - ( angle (C,B,A))))));

      then ( sin (( angle (B,A,C)) + ( angle (C,B,A)))) = ( sin ( PI - (( angle (C,A,D)) - ( angle (C,B,A))))) or ( sin (( angle (B,A,C)) + ( angle (C,B,A)))) = ( sin ( PI - (( angle (C,A,D)) - ( angle (C,B,A))))) by COMPLEX2: 8;

      then ( sin (( angle (B,A,C)) + ( angle (C,B,A)))) = ( sin (( angle (C,A,D)) - ( angle (C,B,A)))) by EUCLID10: 1;

      hence thesis by A1, A2, A3, A4, Th70;

    end;

    theorem :: EUCLID13:90

    (B,C,A) is_a_triangle & ( angle (B,C,A)) < PI & (D,C,A) is_a_triangle & ( angle (C,D,A)) = ( PI / 2) & A in ( LSeg (D,B)) & A <> D implies |.(D - C).| = ((( |.(A - B).| * ( sin ( angle (A,B,C)))) / ( sin (( angle (D,A,C)) - ( angle (A,B,C))))) * ( sin ( angle (D,A,C))))

    proof

      assume that

       A1: (B,C,A) is_a_triangle and

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

       A3: (D,C,A) is_a_triangle and

       A4: ( angle (C,D,A)) = ( PI / 2) and

       A5: A in ( LSeg (D,B)) and

       A6: A <> D;

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

      then

       A7: (( angle (D,A,C)) + ( angle (C,A,B))) = PI or (( angle (D,A,C)) + ( angle (C,A,B))) = (3 * PI ) by A5, A6, EUCLID_6: 13;

      ( sin (( angle (C,A,B)) + ( angle (A,B,C)))) = ( sin (( angle (D,A,C)) - ( angle (A,B,C))))

      proof

        per cases by A7;

          suppose ( angle (C,A,B)) = ( PI - ( angle (D,A,C)));

          

          then ( sin (( angle (C,A,B)) + ( angle (A,B,C)))) = ( sin ( PI - (( angle (D,A,C)) - ( angle (A,B,C)))))

          .= ( sin (( angle (D,A,C)) - ( angle (A,B,C)))) by EUCLID10: 1;

          hence thesis;

        end;

          suppose ( angle (C,A,B)) = ((3 * PI ) - ( angle (D,A,C)));

          

          then ( sin (( angle (C,A,B)) + ( angle (A,B,C)))) = ( sin (((2 * PI ) * 1) + ( PI - (( angle (D,A,C)) - ( angle (A,B,C))))))

          .= ( sin ( PI - (( angle (D,A,C)) - ( angle (A,B,C))))) by COMPLEX2: 8

          .= ( sin (( angle (D,A,C)) - ( angle (A,B,C)))) by EUCLID10: 1;

          hence thesis;

        end;

      end;

      hence thesis by A1, A2, A3, A4, Th71;

    end;