euclid_6.miz

begin

 reserve p1,p2,p3,p4,p5,p6,p,pc for Point of ( TOP-REAL 2);

 reserve a,b,c,r,s for Real;



 Lm1: |.(p1 - p2).| = 0 iff p1 = p2

 proof

 hereby

 assume |.(p1 - p2).| = 0 ;

 then (p1 - p2) = ( 0. ( TOP-REAL 2)) by EUCLID_2: 42;

 hence p1 = p2 by RLVECT_1: 21;

 end;

 assume p1 = p2;

 then (p1 - p2) = ( 0. ( TOP-REAL 2)) by RLVECT_1: 5;

 hence thesis by EUCLID_2: 39;

 end;



 Lm2: |.(p1 - p2).| = |.(p2 - p1).|

 proof

 reconsider q = (p1 - p2) as Element of ( REAL 2) by EUCLID: 22;



 thus |.(p1 - p2).| = |.q qua real-valued FinSequence.|

 .= |.( - q).| by EUCLID: 10

 .= |.( - (p1 - p2)).|

 .= |.(p2 - p1).| by RLVECT_1: 33;

 end;

 theorem :: EUCLID_6:1



 Th1: ( sin ( angle (p1,p2,p3))) = ( sin ( angle (p4,p5,p6))) & ( cos ( angle (p1,p2,p3))) = ( cos ( angle (p4,p5,p6))) implies ( angle (p1,p2,p3)) = ( angle (p4,p5,p6))

 proof



 A1: ((2 * PI ) * 0 ) <= ( angle (p1,p2,p3)) & ( angle (p1,p2,p3)) < ((2 * PI ) + ((2 * PI ) * 0 )) by COMPLEX2: 70;



 A2: ((2 * PI ) * 0 ) <= ( angle (p4,p5,p6)) & ( angle (p4,p5,p6)) < ((2 * PI ) + ((2 * PI ) * 0 )) by COMPLEX2: 70;

 assume ( sin ( angle (p1,p2,p3))) = ( sin ( angle (p4,p5,p6))) & ( cos ( angle (p1,p2,p3))) = ( cos ( angle (p4,p5,p6)));

 hence thesis by A1, A2, SIN_COS6: 61;

 end;

 theorem :: EUCLID_6:2



 Th2: ( sin ( angle (p1,p2,p3))) = ( - ( sin ( angle (p3,p2,p1))))

 proof

 per cases ;

 suppose

 A1: ( angle (p1,p2,p3)) = 0 ;

 then ( angle (p3,p2,p1)) = 0 by EUCLID_3: 36;

 hence thesis by A1, SIN_COS: 31;

 end;

 suppose ( angle (p1,p2,p3)) <> 0 ;

 then ( angle (p3,p2,p1)) = ((2 * PI ) - ( angle (p1,p2,p3))) by EUCLID_3: 37;



 then ( sin ( angle (p1,p2,p3))) = ( sin (( - ( angle (p3,p2,p1))) + (2 * PI )))

 .= ( sin ( - ( angle (p3,p2,p1)))) by SIN_COS: 79

 .= ( - ( sin ( angle (p3,p2,p1)))) by SIN_COS: 31;

 hence thesis;

 end;

 end;

 theorem :: EUCLID_6:3



 Th3: ( cos ( angle (p1,p2,p3))) = ( cos ( angle (p3,p2,p1)))

 proof

 per cases ;

 suppose ( angle (p1,p2,p3)) = 0 ;

 hence thesis by EUCLID_3: 36;

 end;

 suppose ( angle (p1,p2,p3)) <> 0 ;

 then ( angle (p3,p2,p1)) = ((2 * PI ) - ( angle (p1,p2,p3))) by EUCLID_3: 37;



 then ( cos ( angle (p1,p2,p3))) = ( cos (( - ( angle (p3,p2,p1))) + (2 * PI )))

 .= ( cos ( - ( angle (p3,p2,p1)))) by SIN_COS: 79

 .= ( cos ( angle (p3,p2,p1))) by SIN_COS: 31;

 hence thesis;

 end;

 end;



 Lm3: not ( angle (p1,p2,p3)) = ((2 * ( angle (p4,p5,p6))) + (2 * PI ))

 proof

 ( angle (p4,p5,p6)) >= 0 by COMPLEX2: 70;

 then

 A1: ((( angle (p4,p5,p6)) * 2) + (2 * PI )) >= ( 0 + (2 * PI )) by XREAL_1: 7;

 assume ( angle (p1,p2,p3)) = ((2 * ( angle (p4,p5,p6))) + (2 * PI ));

 hence contradiction by A1, COMPLEX2: 70;

 end;



 Lm4: not ( angle (p1,p2,p3)) = ((2 * ( angle (p4,p5,p6))) + (4 * PI ))

 proof

 ( angle (p4,p5,p6)) >= 0 by COMPLEX2: 70;

 then (4 * PI ) >= (2 * PI ) & ((( angle (p4,p5,p6)) * 2) + (4 * PI )) >= ( 0 + (4 * PI )) by XREAL_1: 7, XREAL_1: 64;

 then

 A1: ((( angle (p4,p5,p6)) * 2) + (4 * PI )) >= (2 * PI ) by XXREAL_0: 2;

 assume ( angle (p1,p2,p3)) = ((2 * ( angle (p4,p5,p6))) + (4 * PI ));

 hence contradiction by A1, COMPLEX2: 70;

 end;



 Lm5: not ( angle (p1,p2,p3)) = ((2 * ( angle (p4,p5,p6))) - (4 * PI ))

 proof

 (( angle (p4,p5,p6)) * 2) < ((2 * PI ) * 2) by COMPLEX2: 70, XREAL_1: 68;

 then

 A1: ((( angle (p4,p5,p6)) * 2) - (4 * PI )) < ((4 * PI ) - (4 * PI )) by XREAL_1: 9;

 assume ( angle (p1,p2,p3)) = ((2 * ( angle (p4,p5,p6))) - (4 * PI ));

 hence contradiction by A1, COMPLEX2: 70;

 end;



 Lm6: not ( angle (p1,p2,p3)) = ((2 * ( angle (p4,p5,p6))) - (6 * PI ))

 proof

 (( angle (p4,p5,p6)) * 2) < ((2 * PI ) * 2) by COMPLEX2: 70, XREAL_1: 68;

 then

 A1: ( PI * ( - 2)) <= ( 0 qua Real * ( - 2)) & ((( angle (p4,p5,p6)) * 2) - (6 * PI )) < ((4 * PI ) - (6 * PI )) by XREAL_1: 9;

 assume ( angle (p1,p2,p3)) = ((2 * ( angle (p4,p5,p6))) - (6 * PI ));

 hence contradiction by A1, COMPLEX2: 70;

 end;



 Lm7: for c1,c2 be Element of COMPLEX st c1 = ( euc2cpx (p1 - p2)) & c2 = ( euc2cpx (p3 - p2)) holds ( angle (p1,p2,p3)) = ( angle (c1,c2))

 proof

 let c1,c2 be Element of COMPLEX ;

 assume

 A1: c1 = ( euc2cpx (p1 - p2)) & c2 = ( euc2cpx (p3 - p2));



 thus ( angle (p1,p2,p3)) = ( angle ((p1 - p2),( 0. ( TOP-REAL 2)),(p3 - p2))) by EUCLID_3: 35

 .= ( angle (c1,c2)) by A1, COMPLEX2: 73, EUCLID_3: 17;

 end;



 Lm8: for c1,c2 be Element of COMPLEX st c2 = 0 holds ( Arg ( Rotate (c2,( - ( Arg c1))))) = 0

 proof

 let c1,c2 be Element of COMPLEX ;

 assume c2 = 0 ;

 then ( Rotate (c2,( - ( Arg c1)))) = 0 by COMPLEX2: 52;

 hence thesis by COMPTRIG:def 1;

 end;



 Lm9: for c1,c2 be Element of COMPLEX st c2 = 0 & ( Arg c1) = 0 holds ( angle (c1,c2)) = 0

 proof

 let c1,c2 be Element of COMPLEX ;

 assume that

 A1: c2 = 0 and

 A2: ( Arg c1) = 0 ;



 thus ( angle (c1,c2)) = ( Arg ( Rotate (c2,( - ( Arg c1))))) by A2, COMPLEX2:def 3

 .= 0 by A1, Lm8;

 end;



 Lm10: for c1,c2 be Complex st c2 <> 0 & (( Arg c2) - ( Arg c1)) >= 0 holds ( Arg ( Rotate (c2,( - ( Arg c1))))) = (( Arg c2) - ( Arg c1))

 proof

 let c1,c2 be Complex;

 assume that

 A1: c2 <> 0 and

 A2: (( Arg c2) - ( Arg c1)) >= 0 ;

 set a = (( - ( Arg c1)) + ( Arg c2));

 set z = ( Rotate (c2,( - ( Arg c1))));

 ( Arg c2) < (2 * PI ) & 0 <= ( Arg c1) by COMPTRIG: 34;

 then (( Arg c2) + 0 ) < ((2 * PI ) + ( Arg c1)) by XREAL_1: 8;

 then

 A3: z = (( |.c2.| * ( cos a)) + (( |.c2.| * ( sin a)) * )) & (( Arg c2) - ( Arg c1)) < (((2 * PI ) + ( Arg c1)) - ( Arg c1)) by COMPLEX2:def 2, XREAL_1: 9;



 A4: |.z.| = |.c2.| by COMPLEX2: 53;

 then z <> 0 by A1, COMPLEX1: 44, COMPLEX1: 45;

 hence thesis by A2, A3, A4, COMPTRIG:def 1;

 end;



 Lm11: for c1,c2 be Complex st c2 <> 0 & (( Arg c2) - ( Arg c1)) >= 0 holds ( angle (c1,c2)) = (( Arg c2) - ( Arg c1))

 proof

 let c1,c2 be Complex;

 assume that

 A1: c2 <> 0 and

 A2: (( Arg c2) - ( Arg c1)) >= 0 ;



 thus ( angle (c1,c2)) = ( Arg ( Rotate (c2,( - ( Arg c1))))) by A1, COMPLEX2:def 3

 .= (( Arg c2) - ( Arg c1)) by A1, A2, Lm10;

 end;



 Lm12: for c1,c2 be Element of COMPLEX st c2 <> 0 & (( Arg c2) - ( Arg c1)) < 0 holds ( Arg ( Rotate (c2,( - ( Arg c1))))) = (((2 * PI ) - ( Arg c1)) + ( Arg c2))

 proof

 let c1,c2 be Element of COMPLEX ;

 assume that

 A1: c2 <> 0 and

 A2: (( Arg c2) - ( Arg c1)) < 0 ;

 set a = (( - ( Arg c1)) + ( Arg c2));



 A3: (a + (2 * PI )) < ( 0 + (2 * PI )) by A2, XREAL_1: 6;

 set z = ( Rotate (c2,( - ( Arg c1))));

 z = (( |.c2.| * ( cos a)) + (( |.c2.| * ( sin a)) * )) by COMPLEX2:def 2;



 then

 A4: z = (( |.c2.| * ( cos (((2 * PI ) * 1) + a))) + (( |.c2.| * ( sin a)) * )) by COMPLEX2: 9

 .= (( |.c2.| * ( cos ((2 * PI ) + a))) + (( |.c2.| * ( sin (((2 * PI ) * 1) + a))) * )) by COMPLEX2: 8;

 0 <= ( Arg c2) & ( Arg c1) <= (2 * PI ) by COMPTRIG: 34;

 then (( Arg c1) + 0 ) <= ((2 * PI ) + ( Arg c2)) by XREAL_1: 7;

 then

 A5: (( Arg c1) - ( Arg c1)) <= (((2 * PI ) + ( Arg c2)) - ( Arg c1)) by XREAL_1: 9;



 A6: |.z.| = |.c2.| by COMPLEX2: 53;

 then z <> 0 by A1, COMPLEX1: 44, COMPLEX1: 45;

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

 end;



 Lm13: for c1,c2 be Element of COMPLEX st c2 <> 0 & (( Arg c2) - ( Arg c1)) < 0 holds ( angle (c1,c2)) = (((2 * PI ) - ( Arg c1)) + ( Arg c2))

 proof

 let c1,c2 be Element of COMPLEX ;

 assume that

 A1: c2 <> 0 and

 A2: (( Arg c2) - ( Arg c1)) < 0 ;



 thus ( angle (c1,c2)) = ( Arg ( Rotate (c2,( - ( Arg c1))))) by A1, COMPLEX2:def 3

 .= (((2 * PI ) - ( Arg c1)) + ( Arg c2)) by A1, A2, Lm12;

 end;



 Lm14: for c1,c2,c3 be Element of COMPLEX holds (( angle (c1,c2)) + ( angle (c2,c3))) = ( angle (c1,c3)) or (( angle (c1,c2)) + ( angle (c2,c3))) = (( angle (c1,c3)) + (2 * PI ))

 proof

 let c1,c2,c3 be Element of COMPLEX ;

 per cases ;

 suppose

 A1: c2 = 0 & c3 = 0 ;

 then

 A2: ( Arg c2) = 0 by COMPTRIG:def 1;

 per cases ;

 suppose ( Arg c1) = 0 ;

 then (( angle (c1,c2)) + ( angle (c2,c3))) = ( 0 + ( angle (c2,c3))) by A1, Lm9;

 hence thesis by A1, A2, Lm9;

 end;

 suppose

 A3: ( Arg c1) <> 0 ;



 then (( angle (c1,c2)) + ( angle (c2,c3))) = (((2 * PI ) - ( Arg c1)) + ( angle (c2,c3))) by A1, COMPLEX2:def 3

 .= (((2 * PI ) - ( Arg c1)) + 0 ) by A1, A2, Lm9;

 hence thesis by A1, A3, COMPLEX2:def 3;

 end;

 end;

 suppose

 A4: c2 <> 0 & c3 = 0 ;

 per cases ;

 suppose

 A5: ( Arg c1) = 0 & ( Arg c2) = 0 ;

 per cases ;

 suppose (( Arg c2) - ( Arg c1)) < 0 ;

 hence thesis by A5;

 end;

 suppose (( Arg c2) - ( Arg c1)) >= 0 ;



 then (( angle (c1,c2)) + ( angle (c2,c3))) = ((( Arg c2) - ( Arg c1)) + ( angle (c2,c3))) by A4, Lm11

 .= 0 by A4, A5, Lm9;

 hence thesis by A4, A5, Lm9;

 end;

 end;

 suppose

 A6: ( Arg c1) <> 0 & ( Arg c2) = 0 ;

 per cases ;

 suppose (( Arg c2) - ( Arg c1)) < 0 ;



 then (( angle (c1,c2)) + ( angle (c2,c3))) = ((((2 * PI ) - ( Arg c1)) + ( Arg c2)) + ( angle (c2,c3))) by A4, Lm13

 .= ((2 * PI ) - ( Arg c1)) by A4, A6, Lm9;

 hence thesis by A4, A6, COMPLEX2:def 3;

 end;

 suppose (( Arg c2) - ( Arg c1)) >= 0 ;

 then ( - ( - ( Arg c1))) <= ( - 0 ) by A6;

 hence thesis by A6, COMPTRIG: 34;

 end;

 end;

 suppose

 A7: ( Arg c1) = 0 & ( Arg c2) <> 0 ;

 per cases ;

 suppose (( Arg c2) - ( Arg c1)) < 0 ;

 hence thesis by A7, COMPTRIG: 34;

 end;

 suppose

 A8: (( Arg c2) - ( Arg c1)) >= 0 ;



 A9: ( angle (c1,c3)) = 0 by A4, A7, Lm9;

 (( angle (c1,c2)) + ( angle (c2,c3))) = ((( Arg c2) - ( Arg c1)) + ( angle (c2,c3))) by A4, A8, Lm11

 .= (( Arg c2) + ((2 * PI ) - ( Arg c2))) by A4, A7, COMPLEX2:def 3;

 hence thesis by A9;

 end;

 end;

 suppose

 A10: ( Arg c1) <> 0 & ( Arg c2) <> 0 ;

 per cases ;

 suppose

 A11: (( Arg c2) - ( Arg c1)) < 0 ;



 A12: ( angle (c1,c3)) = ((2 * PI ) - ( Arg c1)) by A4, A10, COMPLEX2:def 3;

 (( angle (c1,c2)) + ( angle (c2,c3))) = ((((2 * PI ) - ( Arg c1)) + ( Arg c2)) + ( angle (c2,c3))) by A4, A11, Lm13

 .= ((((2 * PI ) - ( Arg c1)) + ( Arg c2)) + ((2 * PI ) - ( Arg c2))) by A4, A10, COMPLEX2:def 3

 .= (((2 * PI ) + (2 * PI )) - ( Arg c1));

 hence thesis by A12;

 end;

 suppose

 A13: (( Arg c2) - ( Arg c1)) >= 0 ;



 A14: ( angle (c1,c3)) = ((2 * PI ) - ( Arg c1)) by A4, A10, COMPLEX2:def 3;

 (( angle (c1,c2)) + ( angle (c2,c3))) = ((( Arg c2) - ( Arg c1)) + ( angle (c2,c3))) by A4, A13, Lm11

 .= ((( Arg c2) - ( Arg c1)) + ((2 * PI ) - ( Arg c2))) by A4, A10, COMPLEX2:def 3;

 hence thesis by A14;

 end;

 end;

 end;

 suppose

 A15: c2 = 0 & c3 <> 0 ;

 per cases ;

 suppose (( Arg c3) - ( Arg c2)) < 0 & (( Arg c3) - ( Arg c1)) < 0 ;

 then (( Arg c3) - 0 ) < 0 by A15, COMPTRIG:def 1;

 hence thesis by COMPTRIG: 34;

 end;

 suppose

 A16: (( Arg c3) - ( Arg c2)) >= 0 & (( Arg c3) - ( Arg c1)) < 0 ;

 per cases ;

 suppose ( Arg c1) = 0 ;

 hence thesis by A16, COMPTRIG: 34;

 end;

 suppose ( Arg c1) <> 0 ;



 then (( angle (c1,c2)) + ( angle (c2,c3))) = (((2 * PI ) - ( Arg c1)) + ( angle (c2,c3))) by A15, COMPLEX2:def 3

 .= (((2 * PI ) - ( Arg c1)) + (( Arg c3) - ( Arg c2))) by A15, A16, Lm11

 .= (((2 * PI ) - ( Arg c1)) + (( Arg c3) - 0 )) by A15, COMPTRIG:def 1

 .= (((2 * PI ) - ( Arg c1)) + ( Arg c3));

 hence thesis by A15, A16, Lm13;

 end;

 end;

 suppose (( Arg c3) - ( Arg c2)) < 0 & (( Arg c3) - ( Arg c1)) >= 0 ;

 then (( Arg c3) - 0 ) < 0 by A15, COMPTRIG:def 1;

 hence thesis by COMPTRIG: 34;

 end;

 suppose

 A17: (( Arg c3) - ( Arg c2)) >= 0 & (( Arg c3) - ( Arg c1)) >= 0 ;

 per cases ;

 suppose

 A18: ( Arg c1) = 0 ;



 then (( angle (c1,c2)) + ( angle (c2,c3))) = ( 0 + ( angle (c2,c3))) by A15, Lm9

 .= ( 0 + (( Arg c3) - ( Arg c2))) by A15, A17, Lm11

 .= ( 0 + (( Arg c3) - 0 )) by A15, COMPTRIG:def 1;

 hence thesis by A15, A17, A18, Lm11;

 end;

 suppose

 A19: ( Arg c1) <> 0 ;



 A20: ( angle (c1,c3)) = (( Arg c3) - ( Arg c1)) by A15, A17, Lm11;

 (( angle (c1,c2)) + ( angle (c2,c3))) = (((2 * PI ) - ( Arg c1)) + ( angle (c2,c3))) by A15, A19, COMPLEX2:def 3

 .= (((2 * PI ) - ( Arg c1)) + (( Arg c3) - ( Arg c2))) by A15, A17, Lm11

 .= (((2 * PI ) - ( Arg c1)) + (( Arg c3) - 0 )) by A15, COMPTRIG:def 1;

 hence thesis by A20;

 end;

 end;

 end;

 suppose

 A21: c2 <> 0 & c3 <> 0 ;

 per cases ;

 suppose

 A22: (( Arg c3) - ( Arg c2)) < 0 & (( Arg c3) - ( Arg c1)) < 0 ;

 per cases ;

 suppose

 A23: (( Arg c2) - ( Arg c1)) < 0 ;



 A24: ( angle (c1,c3)) = (((2 * PI ) - ( Arg c1)) + ( Arg c3)) by A21, A22, Lm13;

 (( angle (c1,c2)) + ( angle (c2,c3))) = ((((2 * PI ) - ( Arg c1)) + ( Arg c2)) + ( angle (c2,c3))) by A21, A23, Lm13

 .= ((((2 * PI ) - ( Arg c1)) + ( Arg c2)) + (((2 * PI ) - ( Arg c2)) + ( Arg c3))) by A21, A22, Lm13

 .= ((((2 * PI ) + (2 * PI )) - ( Arg c1)) + ( Arg c3));

 hence thesis by A24;

 end;

 suppose (( Arg c2) - ( Arg c1)) >= 0 ;



 then (( angle (c1,c2)) + ( angle (c2,c3))) = ((( Arg c2) - ( Arg c1)) + ( angle (c2,c3))) by A21, Lm11

 .= ((( Arg c2) - ( Arg c1)) + (((2 * PI ) - ( Arg c2)) + ( Arg c3))) by A21, A22, Lm13

 .= (((2 * PI ) - ( Arg c1)) + ( Arg c3));

 hence thesis by A21, A22, Lm13;

 end;

 end;

 suppose

 A25: (( Arg c3) - ( Arg c2)) >= 0 & (( Arg c3) - ( Arg c1)) < 0 ;

 per cases ;

 suppose (( Arg c2) - ( Arg c1)) < 0 ;



 then (( angle (c1,c2)) + ( angle (c2,c3))) = ((((2 * PI ) - ( Arg c1)) + ( Arg c2)) + ( angle (c2,c3))) by A21, Lm13

 .= ((((2 * PI ) - ( Arg c1)) + ( Arg c2)) + (( Arg c3) - ( Arg c2))) by A21, A25, Lm11

 .= (((2 * PI ) - ( Arg c1)) + ( Arg c3));

 hence thesis by A21, A25, Lm13;

 end;

 suppose (( Arg c2) - ( Arg c1)) >= 0 ;

 then ((( Arg c2) - ( Arg c1)) + (( Arg c3) - ( Arg c2))) >= ( 0 + 0 ) by A25;

 hence thesis by A25;

 end;

 end;

 suppose

 A26: (( Arg c3) - ( Arg c2)) < 0 & (( Arg c3) - ( Arg c1)) >= 0 ;

 per cases ;

 suppose (( Arg c2) - ( Arg c1)) < 0 ;

 then ((( Arg c2) - ( Arg c1)) + (( Arg c3) - ( Arg c2))) < ( 0 + 0 ) by A26;

 hence thesis by A26;

 end;

 suppose

 A27: (( Arg c2) - ( Arg c1)) >= 0 ;



 A28: ( angle (c1,c3)) = (( Arg c3) - ( Arg c1)) by A21, A26, Lm11;

 (( angle (c1,c2)) + ( angle (c2,c3))) = ((( Arg c2) - ( Arg c1)) + ( angle (c2,c3))) by A21, A27, Lm11

 .= ((( Arg c2) - ( Arg c1)) + (((2 * PI ) - ( Arg c2)) + ( Arg c3))) by A21, A26, Lm13

 .= (((2 * PI ) - ( Arg c1)) + ( Arg c3));

 hence thesis by A28;

 end;

 end;

 suppose

 A29: (( Arg c3) - ( Arg c2)) >= 0 & (( Arg c3) - ( Arg c1)) >= 0 ;

 per cases ;

 suppose

 A30: (( Arg c2) - ( Arg c1)) < 0 ;



 A31: ( angle (c1,c3)) = (( Arg c3) - ( Arg c1)) by A21, A29, Lm11;

 (( angle (c1,c2)) + ( angle (c2,c3))) = ((((2 * PI ) - ( Arg c1)) + ( Arg c2)) + ( angle (c2,c3))) by A21, A30, Lm13

 .= ((((2 * PI ) + ( Arg c2)) - ( Arg c1)) + (( Arg c3) - ( Arg c2))) by A21, A29, Lm11

 .= (((2 * PI ) - ( Arg c1)) + ( Arg c3));

 hence thesis by A31;

 end;

 suppose (( Arg c2) - ( Arg c1)) >= 0 ;



 then (( angle (c1,c2)) + ( angle (c2,c3))) = ((( Arg c2) - ( Arg c1)) + ( angle (c2,c3))) by A21, Lm11

 .= ((( Arg c2) - ( Arg c1)) + (( Arg c3) - ( Arg c2))) by A21, A29, Lm11

 .= (( - ( Arg c1)) + ( Arg c3));

 hence thesis by A21, A29, Lm11;

 end;

 end;

 end;

 end;

 theorem :: EUCLID_6:4



 Th4: (( angle (p1,p4,p2)) + ( angle (p2,p4,p3))) = ( angle (p1,p4,p3)) or (( angle (p1,p4,p2)) + ( angle (p2,p4,p3))) = (( angle (p1,p4,p3)) + (2 * PI ))

 proof

 set c1 = ( euc2cpx (p1 - p4));

 set c2 = ( euc2cpx (p2 - p4));

 set c3 = ( euc2cpx (p3 - p4));



 A1: (( angle (c1,c2)) + ( angle (c2,c3))) = ( angle (c1,c3)) or (( angle (c1,c2)) + ( angle (c2,c3))) = (( angle (c1,c3)) + (2 * PI )) by Lm14;

 (( angle (p1,p4,p2)) + ( angle (p2,p4,p3))) = (( angle (c1,c2)) + ( angle (p2,p4,p3))) by Lm7

 .= (( angle (c1,c2)) + ( angle (c2,c3))) by Lm7;

 hence thesis by A1, Lm7;

 end;



 Lm15: ((p1 - p2) `1 ) = ((p1 `1 ) - (p2 `1 )) & ((p1 - p2) `2 ) = ((p1 `2 ) - (p2 `2 ))

 proof

 reconsider pp = p2 as Element of ( REAL 2) by EUCLID: 22;



 A1: (( - p2) `1 ) = (( - pp) . 1)

 .= ( - (pp . 1)) by VALUED_1: 8

 .= ( - (p2 `1 ));



 A2: ( euc2cpx (p1 - p2)) = (( euc2cpx p1) - ( euc2cpx p2)) by EUCLID_3: 15

 .= (( euc2cpx p1) + ( - ( euc2cpx p2)))

 .= (( euc2cpx p1) + ( euc2cpx ( - p2))) by EUCLID_3: 13;



 hence ((p1 - p2) `1 ) = ( Re (( euc2cpx p1) + ( euc2cpx ( - p2)))) by COMPLEX1: 12

 .= (( Re ( euc2cpx p1)) + ( Re ( euc2cpx ( - p2)))) by COMPLEX1: 8

 .= ((p1 `1 ) + ( Re ( euc2cpx ( - p2)))) by COMPLEX1: 12

 .= ((p1 `1 ) + (( - p2) `1 )) by COMPLEX1: 12

 .= ((p1 `1 ) - (p2 `1 )) by A1;



 A3: (( - p2) `2 ) = (( - pp) . 2)

 .= ( - (pp . 2)) by VALUED_1: 8

 .= ( - (p2 `2 ));



 thus ((p1 - p2) `2 ) = ( Im (( euc2cpx p1) + ( euc2cpx ( - p2)))) by A2, COMPLEX1: 12

 .= (( Im ( euc2cpx p1)) + ( Im ( euc2cpx ( - p2)))) by COMPLEX1: 8

 .= ((p1 `2 ) + ( Im ( euc2cpx ( - p2)))) by COMPLEX1: 12

 .= ((p1 `2 ) + (( - p2) `2 )) by COMPLEX1: 12

 .= ((p1 `2 ) - (p2 `2 )) by A3;

 end;



 Lm16: for c1,c2 be Element of COMPLEX st c1 = ( euc2cpx (p1 - p2)) & c2 = ( euc2cpx (p3 - p2)) holds ( Re (c1 .|. c2)) = ((((p1 `1 ) - (p2 `1 )) * ((p3 `1 ) - (p2 `1 ))) + (((p1 `2 ) - (p2 `2 )) * ((p3 `2 ) - (p2 `2 )))) & ( Im (c1 .|. c2)) = (( - (((p1 `1 ) - (p2 `1 )) * ((p3 `2 ) - (p2 `2 )))) + (((p1 `2 ) - (p2 `2 )) * ((p3 `1 ) - (p2 `1 )))) & |.c1.| = ( sqrt ((((p1 `1 ) - (p2 `1 )) ^2 ) + (((p1 `2 ) - (p2 `2 )) ^2 ))) & |.(p1 - p2).| = |.c1.|

 proof

 let c1,c2 be Element of COMPLEX ;

 assume that

 A1: c1 = ( euc2cpx (p1 - p2)) and

 A2: c2 = ( euc2cpx (p3 - p2));



 A3: ( Re c2) = ((p3 - p2) `1 ) by A2, COMPLEX1: 12

 .= ((p3 `1 ) - (p2 `1 )) by Lm15;



 A4: ( Im c2) = ((p3 - p2) `2 ) by A2, COMPLEX1: 12

 .= ((p3 `2 ) - (p2 `2 )) by Lm15;



 A5: ( Im c1) = ((p1 - p2) `2 ) by A1, COMPLEX1: 12

 .= ((p1 `2 ) - (p2 `2 )) by Lm15;



 A6: ( Re c1) = ((p1 - p2) `1 ) by A1, COMPLEX1: 12

 .= ((p1 `1 ) - (p2 `1 )) by Lm15;

 hence ( Re (c1 .|. c2)) = ((((p1 `1 ) - (p2 `1 )) * ((p3 `1 ) - (p2 `1 ))) + (((p1 `2 ) - (p2 `2 )) * ((p3 `2 ) - (p2 `2 )))) by A3, A5, A4, EUCLID_3: 39;

 thus ( Im (c1 .|. c2)) = (( - (((p1 `1 ) - (p2 `1 )) * ((p3 `2 ) - (p2 `2 )))) + (((p1 `2 ) - (p2 `2 )) * ((p3 `1 ) - (p2 `1 )))) by A6, A3, A5, A4, EUCLID_3: 40;



 thus |.c1.| = ( sqrt ((((p1 - p2) `1 ) ^2 ) + (( Im c1) ^2 ))) by A1, COMPLEX1: 12

 .= ( sqrt ((((p1 - p2) `1 ) ^2 ) + (((p1 - p2) `2 ) ^2 ))) by A1, COMPLEX1: 12

 .= ( sqrt ((((p1 `1 ) - (p2 `1 )) ^2 ) + (((p1 - p2) `2 ) ^2 ))) by Lm15

 .= ( sqrt ((((p1 `1 ) - (p2 `1 )) ^2 ) + (((p1 `2 ) - (p2 `2 )) ^2 ))) by Lm15;

 thus thesis by A1, EUCLID_3: 25;

 end;

 definition

 let p1, p2, p3;

 ::$Notion-Name

 :: EUCLID_6:def1

 func the_area_of_polygon3 (p1,p2,p3) -> Real equals ((((((p1 `1 ) * (p2 `2 )) - ((p2 `1 ) * (p1 `2 ))) + (((p2 `1 ) * (p3 `2 )) - ((p3 `1 ) * (p2 `2 )))) + (((p3 `1 ) * (p1 `2 )) - ((p1 `1 ) * (p3 `2 )))) / 2);

 correctness ;

 end

 definition

 let p1, p2, p3;

 :: EUCLID_6:def2

 func the_perimeter_of_polygon3 (p1,p2,p3) -> Real equals (( |.(p2 - p1).| + |.(p3 - p2).|) + |.(p1 - p3).|);

 correctness ;

 end

 theorem :: EUCLID_6:5



 Th5: ( the_area_of_polygon3 (p1,p2,p3)) = ((( |.(p1 - p2).| * |.(p3 - p2).|) * ( sin ( angle (p3,p2,p1)))) / 2)

 proof

 per cases ;

 suppose

 A1: p1 = p2;



 then |.(p1 - p2).| = |.( 0. ( TOP-REAL 2)).| by RLVECT_1: 5

 .= 0 by EUCLID_2: 39;

 hence thesis by A1;

 end;

 suppose

 A2: p1 <> p2;

 per cases ;

 suppose

 A3: p2 = p3;



 then |.(p3 - p2).| = |.( 0. ( TOP-REAL 2)).| by RLVECT_1: 5

 .= 0 by EUCLID_2: 39;

 hence thesis by A3;

 end;

 suppose

 A4: p2 <> p3;

 set b = ( euc2cpx (p3 - p2));

 set a = ( euc2cpx (p1 - p2));

 A5:

 now

 assume

 A6: a = 0 or b = 0 ;

 per cases by A6;

 suppose a = 0 ;

 hence contradiction by A2, EUCLID_3: 18, RLVECT_1: 21;

 end;

 suppose b = 0 ;

 hence contradiction by A4, EUCLID_3: 18, RLVECT_1: 21;

 end;

 end;

 A7:

 now

 assume

 A8: ( |.a.| * |.b.|) = 0 ;

 per cases by A8;

 suppose |.a.| = 0 ;

 hence contradiction by A5, COMPLEX1: 45;

 end;

 suppose |.b.| = 0 ;

 hence contradiction by A5, COMPLEX1: 45;

 end;

 end;

 ((( |.(p1 - p2).| * |.(p3 - p2).|) * ( sin ( angle (p3,p2,p1)))) / 2) = ((( |.(p1 - p2).| * |.(p3 - p2).|) * ( - ( sin ( angle (p1,p2,p3))))) / 2) by Th2

 .= ((( |.(p1 - p2).| * |.(p3 - p2).|) * ( - ( sin ( angle (a,b))))) / 2) by Lm7

 .= ((( |.(p1 - p2).| * |.(p3 - p2).|) * ( - ( - (( Im (a .|. b)) / ( |.a.| * |.b.|))))) / 2) by A5, COMPLEX2: 69

 .= ((( |.a.| * |.(p3 - p2).|) * (( Im (a .|. b)) / ( |.a.| * |.b.|))) / 2) by Lm16

 .= ((( |.a.| * |.b.|) * (( Im (a .|. b)) / ( |.a.| * |.b.|))) / 2) by Lm16

 .= ((( Im (a .|. b)) / (( |.a.| * |.b.|) / ( |.a.| * |.b.|))) / 2) by XCMPLX_1: 81

 .= ((( Im (a .|. b)) / 1) / 2) by A7, XCMPLX_1: 60

 .= ((( - (((p1 `1 ) - (p2 `1 )) * ((p3 `2 ) - (p2 `2 )))) + (((p1 `2 ) - (p2 `2 )) * ((p3 `1 ) - (p2 `1 )))) / 2) by Lm16

 .= ((((((p1 `1 ) * (p2 `2 )) - ((p2 `1 ) * (p1 `2 ))) + (((p2 `1 ) * (p3 `2 )) - ((p3 `1 ) * (p2 `2 )))) + (((p3 `1 ) * (p1 `2 )) - ((p1 `1 ) * (p3 `2 )))) / 2);

 hence thesis;

 end;

 end;

 end;

 theorem :: EUCLID_6:6



 Th6: p2 <> p1 implies ( |.(p3 - p2).| * ( sin ( angle (p3,p2,p1)))) = ( |.(p3 - p1).| * ( sin ( angle (p2,p1,p3))))

 proof

 ( the_area_of_polygon3 (p1,p2,p3)) = ( the_area_of_polygon3 (p3,p1,p2));

 then ((( |.(p1 - p2).| * |.(p3 - p2).|) * ( sin ( angle (p3,p2,p1)))) / 2) = ( the_area_of_polygon3 (p3,p1,p2)) by Th5;

 then ((( |.(p1 - p2).| * |.(p3 - p2).|) * ( sin ( angle (p3,p2,p1)))) / 2) = ((( |.(p3 - p1).| * |.(p2 - p1).|) * ( sin ( angle (p2,p1,p3)))) / 2) by Th5;

 then (( |.(p1 - p2).| * |.(p3 - p2).|) * ( sin ( angle (p3,p2,p1)))) = (( |.(p3 - p1).| * |.(p1 - p2).|) * ( sin ( angle (p2,p1,p3)))) by Lm2;

 then

 A1: (( |.(p3 - p2).| * ( sin ( angle (p3,p2,p1)))) * |.(p1 - p2).|) = (( |.(p3 - p1).| * ( sin ( angle (p2,p1,p3)))) * |.(p1 - p2).|);

 assume p2 <> p1;

 then |.(p1 - p2).| <> 0 by Lm1;

 hence thesis by A1, XCMPLX_1: 5;

 end;

 ::$Notion-Name

 theorem :: EUCLID_6:7



 Th7: a = |.(p1 - p2).| & b = |.(p3 - p2).| & c = |.(p3 - p1).| implies (c ^2 ) = (((a ^2 ) + (b ^2 )) - (((2 * a) * b) * ( cos ( angle (p1,p2,p3)))))

 proof

 assume that

 A1: a = |.(p1 - p2).| & b = |.(p3 - p2).| and

 A2: c = |.(p3 - p1).|;

 per cases ;

 suppose

 A3: p1 = p2;



 then |.(p1 - p2).| = |.( 0. ( TOP-REAL 2)).| by RLVECT_1: 5

 .= 0 by EUCLID_2: 39;

 hence thesis by A1, A2, A3;

 end;

 suppose

 A4: p1 <> p2;

 per cases ;

 suppose

 A5: p2 = p3;



 then |.(p3 - p2).| = |.( 0. ( TOP-REAL 2)).| by RLVECT_1: 5

 .= 0 by EUCLID_2: 39;



 then ((( |.(p1 - p2).| ^2 ) + ( |.(p3 - p2).| ^2 )) - (((2 * |.(p1 - p2).|) * |.(p3 - p2).|) * ( cos ( angle (p1,p2,p3))))) = ( |.( - (p1 - p2)).| ^2 ) by EUCLID: 71

 .= ( |.(p2 - p1).| ^2 ) by RLVECT_1: 33;

 hence thesis by A1, A2, A5;

 end;

 suppose

 A6: p2 <> p3;

 set c2 = ( euc2cpx (p3 - p2));

 set c1 = ( euc2cpx (p1 - p2));

 A7:

 now

 assume

 A8: c1 = 0 or c2 = 0 ;

 per cases by A8;

 suppose c1 = 0 ;

 hence contradiction by A4, EUCLID_3: 18, RLVECT_1: 21;

 end;

 suppose c2 = 0 ;

 hence contradiction by A6, EUCLID_3: 18, RLVECT_1: 21;

 end;

 end;

 A9:

 now

 assume

 A10: ( |.c1.| * |.c2.|) = 0 ;

 per cases by A10;

 suppose |.c1.| = 0 ;

 hence contradiction by A7, COMPLEX1: 45;

 end;

 suppose |.c2.| = 0 ;

 hence contradiction by A7, COMPLEX1: 45;

 end;

 end;



 A11: (((a ^2 ) + (b ^2 )) - (c ^2 )) = ((((( |.p1.| ^2 ) - (2 * |(p2, p1)|)) + ( |.p2.| ^2 )) + ( |.(p3 - p2).| ^2 )) - ( |.(p3 - p1).| ^2 )) by A1, A2, EUCLID_2: 46

 .= ((((( |.p1.| ^2 ) - (2 * |(p2, p1)|)) + ( |.p2.| ^2 )) + ( |.(p3 - p2).| ^2 )) - ((( |.p3.| ^2 ) - (2 * |(p1, p3)|)) + ( |.p1.| ^2 ))) by EUCLID_2: 46

 .= ((((( - (2 * |(p2, p1)|)) + ( |.p2.| ^2 )) + ( |.(p3 - p2).| ^2 )) - ( |.p3.| ^2 )) + (2 * |(p1, p3)|))

 .= ((((( - (2 * |(p2, p1)|)) + ( |.p2.| ^2 )) + ((( |.p3.| ^2 ) - (2 * |(p2, p3)|)) + ( |.p2.| ^2 ))) - ( |.p3.| ^2 )) + (2 * |(p1, p3)|)) by EUCLID_2: 46

 .= (2 * (((( - |(p2, p1)|) + ( |.p2.| ^2 )) - |(p2, p3)|) + |(p1, p3)|));

 (( |.(p1 - p2).| * |.(p3 - p2).|) * ( cos ( angle (p1,p2,p3)))) = (( |.(p1 - p2).| * |.(p3 - p2).|) * ( cos ( angle (c1,c2)))) by Lm7

 .= (( |.c1.| * |.(p3 - p2).|) * ( cos ( angle (c1,c2)))) by Lm16

 .= (( |.c1.| * |.c2.|) * ( cos ( angle (c1,c2)))) by Lm16

 .= (( |.c1.| * |.c2.|) * (( Re (c1 .|. c2)) / ( |.c1.| * |.c2.|))) by A7, COMPLEX2: 69

 .= (( Re (c1 .|. c2)) / (( |.c1.| * |.c2.|) / ( |.c1.| * |.c2.|))) by XCMPLX_1: 81

 .= (( Re (c1 .|. c2)) / 1) by A9, XCMPLX_1: 60

 .= ((((p1 `1 ) - (p2 `1 )) * ((p3 `1 ) - (p2 `1 ))) + (((p1 `2 ) - (p2 `2 )) * ((p3 `2 ) - (p2 `2 )))) by Lm16

 .= (((((((p1 `1 ) * (p3 `1 )) + ((p1 `2 ) * (p3 `2 ))) - ((p1 `1 ) * (p2 `1 ))) - ((p2 `1 ) * (p3 `1 ))) + ((p2 `1 ) * (p2 `1 ))) + ((( - ((p1 `2 ) * (p2 `2 ))) - ((p2 `2 ) * (p3 `2 ))) + ((p2 `2 ) * (p2 `2 ))))

 .= (((( |(p1, p3)| - ((p1 `1 ) * (p2 `1 ))) - ((p2 `1 ) * (p3 `1 ))) + ((p2 `1 ) * (p2 `1 ))) + ((( - ((p1 `2 ) * (p2 `2 ))) - ((p2 `2 ) * (p3 `2 ))) + ((p2 `2 ) * (p2 `2 )))) by EUCLID_3: 41

 .= (((( |(p1, p3)| - (((p1 `1 ) * (p2 `1 )) + ((p1 `2 ) * (p2 `2 )))) - ((p2 `1 ) * (p3 `1 ))) + ((p2 `1 ) * (p2 `1 ))) + (( - ((p2 `2 ) * (p3 `2 ))) + ((p2 `2 ) * (p2 `2 ))))

 .= (((( |(p1, p3)| - |(p1, p2)|) - ((p2 `1 ) * (p3 `1 ))) + ((p2 `1 ) * (p2 `1 ))) + (( - ((p2 `2 ) * (p3 `2 ))) + ((p2 `2 ) * (p2 `2 )))) by EUCLID_3: 41

 .= (((( |(p1, p3)| - |(p1, p2)|) - (((p2 `1 ) * (p3 `1 )) + ((p2 `2 ) * (p3 `2 )))) + ((p2 `1 ) * (p2 `1 ))) + ((p2 `2 ) * (p2 `2 )))

 .= (((( |(p1, p3)| - |(p1, p2)|) - |(p2, p3)|) + ((p2 `1 ) * (p2 `1 ))) + ((p2 `2 ) * (p2 `2 ))) by EUCLID_3: 41

 .= ((( |(p1, p3)| - |(p1, p2)|) - |(p2, p3)|) + (((p2 `1 ) * (p2 `1 )) + ((p2 `2 ) * (p2 `2 ))))

 .= ((( |(p1, p3)| - |(p1, p2)|) - |(p2, p3)|) + |(p2, p2)|) by EUCLID_3: 41

 .= ((( |(p1, p3)| - |(p1, p2)|) - |(p2, p3)|) + ( |.p2.| ^2 )) by EUCLID_2: 36;

 hence thesis by A1, A11;

 end;

 end;

 end;

 begin

 theorem :: EUCLID_6:8



 Th8: p in ( LSeg (p1,p2)) & p <> p1 & p <> p2 implies ( angle (p1,p,p2)) = PI

 proof

 set c1 = ( euc2cpx (p1 - p));

 set c2 = ( euc2cpx (p2 - p));

 assume p in ( LSeg (p1,p2));

 then

 consider l be Real such that

 A1: p = (((1 - l) * p1) + (l * p2)) and

 A2: 0 <= l and

 A3: l <= 1;

 reconsider l as Real;



 A4: (p2 - p) = (p2 - (((1 + ( - l)) * p1) + (l * p2))) by A1

 .= (p2 - (((1 * p1) + (( - l) * p1)) + (l * p2))) by RLVECT_1:def 6

 .= (p2 + (( - 1) * (((1 * p1) + (( - l) * p1)) + (l * p2))))

 .= (p2 + ((( - 1) * ((1 * p1) + (( - l) * p1))) + (( - 1) * (l * p2)))) by RLVECT_1:def 5

 .= (p2 + ((( - 1) * (p1 + (( - l) * p1))) + (( - 1) * (l * p2)))) by RLVECT_1:def 8

 .= (p2 + ((( - 1) * (p1 + (( - l) * p1))) + ((( - 1) * l) * p2))) by RLVECT_1:def 7

 .= (p2 + (((( - 1) * p1) + (( - 1) * (( - l) * p1))) + (( - l) * p2))) by RLVECT_1:def 5

 .= (p2 + (((( - 1) * p1) + ((( - 1) * ( - l)) * p1)) + (( - l) * p2))) by RLVECT_1:def 7

 .= (p2 + ((( - 1) * p1) + ((l * p1) + (( - l) * p2)))) by RLVECT_1:def 3

 .= (p2 + (( - p1) + ((l * p1) + (( - l) * p2))))

 .= ((( - p1) + p2) + ((l * p1) + (( - l) * p2))) by RLVECT_1:def 3

 .= ((( - p1) + p2) + ((l * ( - ( - p1))) + (( - l) * p2)))

 .= ((( - p1) + p2) + ((l * (( - 1) * ( - p1))) + (( - l) * p2)))

 .= ((( - p1) + p2) + (((l * ( - 1)) * ( - p1)) + (( - l) * p2))) by RLVECT_1:def 7

 .= ((( - p1) + p2) + (( - l) * (( - p1) + p2))) by RLVECT_1:def 5

 .= ((1 * (( - p1) + p2)) + (( - l) * (( - p1) + p2))) by RLVECT_1:def 8

 .= ((1 + ( - l)) * (( - p1) + p2)) by RLVECT_1:def 6

 .= ((1 - l) * (( - p1) + p2));

 assume

 A5: p <> p1;



 A6: l <> 0

 proof

 assume l = 0 ;



 then p = ((1 * p1) + ( 0. ( TOP-REAL 2))) by A1, RLVECT_1: 10

 .= (1 * p1) by RLVECT_1: 4

 .= p1 by RLVECT_1:def 8;

 hence contradiction by A5;

 end;

 assume

 A7: p <> p2;

 l <> 1

 proof

 assume l = 1;



 then p = (( 0. ( TOP-REAL 2)) + (1 * p2)) by A1, RLVECT_1: 10

 .= (1 * p2) by RLVECT_1: 4

 .= p2 by RLVECT_1:def 8;

 hence contradiction by A7;

 end;

 then l < 1 by A3, XXREAL_0: 1;

 then ( - 1) < ( - l) by XREAL_1: 24;

 then

 A8: (( - 1) + 1) < (( - l) + 1) by XREAL_1: 6;



 A9: ( - c2) <> 0

 proof

 assume ( - c2) = 0 ;

 then |.(p2 - p).| = 0 by COMPLEX1: 44, EUCLID_3: 25;

 then (p2 - p) = ( 0. ( TOP-REAL 2)) by EUCLID_2: 42;

 hence contradiction by A7, RLVECT_1: 21;

 end;

 set r = ( - (l / (1 - l)));



 A10: (p1 - p) = (p1 - (((1 + ( - l)) * p1) + (l * p2))) by A1

 .= (p1 - (((1 * p1) + (( - l) * p1)) + (l * p2))) by RLVECT_1:def 6

 .= (p1 + (( - 1) * (((1 * p1) + (( - l) * p1)) + (l * p2))))

 .= (p1 + ((( - 1) * ((1 * p1) + (( - l) * p1))) + (( - 1) * (l * p2)))) by RLVECT_1:def 5

 .= (p1 + ((( - 1) * (p1 + (( - l) * p1))) + (( - 1) * (l * p2)))) by RLVECT_1:def 8

 .= (p1 + ((( - 1) * (p1 + (( - l) * p1))) + ((( - 1) * l) * p2))) by RLVECT_1:def 7

 .= (p1 + (((( - 1) * p1) + (( - 1) * (( - l) * p1))) + (( - l) * p2))) by RLVECT_1:def 5

 .= (p1 + (((( - 1) * p1) + ((( - 1) * ( - l)) * p1)) + (( - l) * p2))) by RLVECT_1:def 7

 .= (p1 + ((( - 1) * p1) + ((l * p1) + (( - l) * p2)))) by RLVECT_1:def 3

 .= (p1 + (( - p1) + ((l * p1) + (( - l) * p2))))

 .= ((p1 + ( - p1)) + ((l * p1) + (( - l) * p2))) by RLVECT_1:def 3

 .= (( 0. ( TOP-REAL 2)) + ((l * p1) + (( - l) * p2))) by RLVECT_1: 5

 .= ((l * p1) + ((l * ( - 1)) * p2)) by RLVECT_1: 4

 .= ((l * p1) + (l * (( - 1) * p2))) by RLVECT_1:def 7

 .= ((l * p1) + (l * ( - p2)))

 .= (l * (p1 - p2)) by RLVECT_1:def 5;

 ( cpx2euc (c2 * r)) = (r * ( cpx2euc c2)) by EUCLID_3: 19

 .= (( - (l / (1 - l))) * ((1 - l) * (( - p1) + p2))) by A4, EUCLID_3: 2

 .= ((( - (l / (1 - l))) * (1 - l)) * (( - p1) + p2)) by RLVECT_1:def 7

 .= (((( - l) / (1 - l)) * (1 - l)) * (( - p1) + p2)) by XCMPLX_1: 187

 .= ((((1 - l) / (1 - l)) * ( - l)) * (( - p1) + p2)) by XCMPLX_1: 75

 .= ((1 * ( - l)) * (( - p1) + p2)) by A8, XCMPLX_1: 60

 .= ((l * ( - 1)) * (( - p1) + p2))

 .= (l * (( - 1) * (( - p1) + p2))) by RLVECT_1:def 7

 .= (l * ((( - 1) * ( - p1)) + (( - 1) * p2))) by RLVECT_1:def 5

 .= (l * (( - ( - p1)) + (( - 1) * p2)))

 .= (l * (( - ( - p1)) + ( - p2)))

 .= (l * (( - ( - p1)) + ( - p2)))

 .= (l * (p1 + ( - p2)))

 .= ( cpx2euc c1) by A10, EUCLID_3: 2;

 then c1 = (c2 * r) by EUCLID_3: 3;

 then

 A11: ( Arg ( - c2)) = ( Arg c1) by A2, A6, A8, COMPLEX2: 28;

 ( angle (c1,( - c2))) = 0

 proof

 per cases ;

 suppose (( Arg ( - c2)) - ( Arg c1)) < 0 ;

 hence thesis by A11;

 end;

 suppose (( Arg ( - c2)) - ( Arg c1)) >= 0 ;

 hence thesis by A11, A9, Lm11;

 end;

 end;

 then ( angle (c1,( - ( - c2)))) = PI by A9, COMPLEX2: 68;

 hence thesis by Lm7;

 end;

 theorem :: EUCLID_6:9



 Th9: p in ( LSeg (p2,p3)) & p <> p2 implies ( angle (p3,p2,p1)) = ( angle (p,p2,p1))

 proof

 set c = ( euc2cpx (p - p2));

 set c1 = ( euc2cpx (p1 - p2));

 set c3 = ( euc2cpx (p3 - p2));

 assume p in ( LSeg (p2,p3));

 then

 consider l be Real such that

 A1: p = (((1 - l) * p2) + (l * p3)) and

 A2: 0 <= l and l <= 1;

 reconsider l as Real;



 A3: (p - p2) = ((((1 + ( - l)) * p2) + (l * p3)) - p2) by A1

 .= ((((1 * p2) + (( - l) * p2)) + (l * p3)) - p2) by RLVECT_1:def 6

 .= (((p2 + (( - l) * p2)) + (l * p3)) - p2) by RLVECT_1:def 8

 .= ((p2 + (( - l) * p2)) + ((l * p3) + ( - p2))) by RLVECT_1:def 3

 .= (p2 + ((( - l) * p2) + ((l * p3) + ( - p2)))) by RLVECT_1:def 3

 .= (p2 + (( - p2) + ((( - l) * p2) + (l * p3)))) by RLVECT_1:def 3

 .= ((p2 + ( - p2)) + ((( - l) * p2) + (l * p3))) by RLVECT_1:def 3

 .= (( 0. ( TOP-REAL 2)) + ((( - l) * p2) + (l * p3))) by RLVECT_1: 5

 .= (((l * ( - 1)) * p2) + (l * p3)) by RLVECT_1: 4

 .= ((l * (( - 1) * p2)) + (l * p3)) by RLVECT_1:def 7

 .= ((l * ( - p2)) + (l * p3))

 .= (l * (p3 - p2)) by RLVECT_1:def 5;

 assume

 A4: p <> p2;



 A5: l <> 0

 proof

 assume l = 0 ;



 then p = ((1 * p2) + ( 0. ( TOP-REAL 2))) by A1, RLVECT_1: 10

 .= (1 * p2) by RLVECT_1: 4

 .= p2 by RLVECT_1:def 8;

 hence contradiction by A4;

 end;

 ( cpx2euc (c3 * l)) = (l * ( cpx2euc c3)) by EUCLID_3: 19

 .= (l * (p3 - p2)) by EUCLID_3: 2

 .= ( cpx2euc c) by A3, EUCLID_3: 2;

 then c = (c3 * l) by EUCLID_3: 3;

 then

 A6: ( Arg c) = ( Arg c3) by A2, A5, COMPLEX2: 27;

 ( angle (c3,c1)) = ( angle (c,c1))

 proof

 per cases ;

 suppose

 A7: ( Arg c3) = 0 or c1 <> 0 ;



 then ( angle (c3,c1)) = ( Arg ( Rotate (c1,( - ( Arg c3))))) by COMPLEX2:def 3

 .= ( angle (c,c1)) by A6, A7, COMPLEX2:def 3;

 hence thesis;

 end;

 suppose

 A8: not (( Arg c3) = 0 or c1 <> 0 );



 then ( angle (c3,c1)) = ((2 * PI ) - ( Arg c3)) by COMPLEX2:def 3

 .= ( angle (c,c1)) by A6, A8, COMPLEX2:def 3;

 hence thesis;

 end;

 end;



 hence ( angle (p3,p2,p1)) = ( angle (c,c1)) by Lm7

 .= ( angle (p,p2,p1)) by Lm7;

 end;

 theorem :: EUCLID_6:10



 Th10: p in ( LSeg (p2,p3)) & p <> p2 implies ( angle (p1,p2,p3)) = ( angle (p1,p2,p))

 proof

 assume

 A1: p in ( LSeg (p2,p3));

 assume

 A2: p <> p2;

 then

 A3: ( angle (p3,p2,p1)) = ( angle (p,p2,p1)) by A1, Th9;

 per cases ;

 suppose

 A4: ( angle (p1,p2,p3)) = 0 ;

 then ( angle (p3,p2,p1)) = 0 by EUCLID_3: 36;

 then

 A5: ( angle (p,p2,p1)) = 0 by A1, A2, Th9;



 thus ( angle (p1,p2,p3)) = ( angle (p3,p2,p1)) by A4, EUCLID_3: 36

 .= ( angle (p,p2,p1)) by A1, A2, Th9

 .= ( angle (p1,p2,p)) by A5, EUCLID_3: 36;

 end;

 suppose

 A6: ( angle (p1,p2,p3)) <> 0 ;

 then

 A7: ( angle (p,p2,p1)) <> 0 by A3, EUCLID_3: 36;



 thus ( angle (p1,p2,p3)) = ((2 * PI ) - ( angle (p3,p2,p1))) by A6, EUCLID_3: 38

 .= ((2 * PI ) - ( angle (p,p2,p1))) by A1, A2, Th9

 .= ( angle (p1,p2,p)) by A7, EUCLID_3: 37;

 end;

 end;



 Lm17: p1 in ( inside_of_circle (a,b,r)) & p2 in ( outside_of_circle (a,b,r)) implies ex p st p in (( LSeg (p1,p2)) /\ ( circle (a,b,r)))

 proof

 set pc1 = (p1 - |[a, b]|);

 set pc2 = (p2 - |[a, b]|);

 reconsider r9 = r as Real;

 assume p1 in ( inside_of_circle (a,b,r));

 then p1 in { p : |.(p - |[a, b]|).| < r } by JGRAPH_6:def 6;

 then

 A1: ex p19 be Point of ( TOP-REAL 2) st p1 = p19 & |.(p19 - |[a, b]|).| < r;

 assume p2 in ( outside_of_circle (a,b,r));

 then p2 in { p : |.(p - |[a, b]|).| > r } by JGRAPH_6:def 8;

 then

 A2: ex p29 be Point of ( TOP-REAL 2) st p2 = p29 & |.(p29 - |[a, b]|).| > r;

 then

 consider f be Function of I[01] , (( TOP-REAL 2) | ( LSeg (pc1,pc2))) such that

 A3: for x be Real st x in [. 0 , 1.] holds (f . x) = (((1 - x) * pc1) + (x * pc2)) and

 A4: f is being_homeomorphism and

 A5: (f . 0 ) = pc1 and

 A6: (f . 1) = pc2 by A1, JORDAN5A: 3;

 reconsider g = f as Function of I[01] , ( TOP-REAL 2) by JORDAN6: 3;

 0 in the carrier of I[01] by BORSUK_1: 40, XXREAL_1: 1;

 then 0 in ( dom g) by FUNCT_2:def 1;

 then

 A7: (g /. 0 ) = pc1 by A5, PARTFUN1:def 6;

 1 in the carrier of I[01] by BORSUK_1: 40, XXREAL_1: 1;

 then 1 in ( dom g) by FUNCT_2:def 1;

 then

 A8: (g /. 1) = pc2 by A6, PARTFUN1:def 6;

 f is continuous by A4, TOPS_2:def 5;

 then

 consider s be Point of I[01] such that

 A9: |.(g /. s).| = r9 by A1, A2, A7, A8, JORDAN2C: 86, JORDAN6: 3;



 A10: s in the carrier of I[01] ;

 s in [. 0 , 1.] by BORSUK_1: 40;

 then s in { s9 where s9 be Element of ExtREAL : 0 <= s9 & s9 <= 1 } by XXREAL_1:def 1;

 then

 A11: ex s9 be Element of ExtREAL st s = s9 & 0 <= s9 & s9 <= 1;

 reconsider s as Real;

 set p9 = (f . s);

 s in ( dom g) by A10, FUNCT_2:def 1;

 then ( rng g) c= the carrier of ( TOP-REAL 2) & (g . s) in ( rng g) by FUNCT_1: 3, RELAT_1:def 19;

 then

 reconsider p9 as Point of ( TOP-REAL 2);

 set p = (p9 + |[a, b]|);

 take p;

 (f . s) = (((1 - s) * pc1) + (s * pc2)) by A3, BORSUK_1: 40

 .= ((((1 - s) * p1) - ((1 - s) * |[a, b]|)) + (s * (p2 - |[a, b]|))) by RLVECT_1: 34

 .= ((((1 - s) * p1) - ((1 - s) * |[a, b]|)) + ((s * p2) - (s * |[a, b]|))) by RLVECT_1: 34

 .= ((((1 - s) * p1) + (( - (1 - s)) * |[a, b]|)) + ((s * p2) - (s * |[a, b]|))) by RLVECT_1: 79

 .= ((((1 - s) * p1) + ((( - 1) + s) * |[a, b]|)) + ((s * p2) - (s * |[a, b]|)))

 .= ((((1 - s) * p1) + ((( - 1) * |[a, b]|) + (s * |[a, b]|))) + ((s * p2) - (s * |[a, b]|))) by RLVECT_1:def 6

 .= (((((1 - s) * p1) + (( - 1) * |[a, b]|)) + (s * |[a, b]|)) + ((s * p2) + ( - (s * |[a, b]|)))) by RLVECT_1:def 3

 .= ((((1 - s) * p1) + (( - 1) * |[a, b]|)) + ((s * |[a, b]|) + ((s * p2) + ( - (s * |[a, b]|))))) by RLVECT_1:def 3

 .= ((((1 - s) * p1) + (( - 1) * |[a, b]|)) + (((s * |[a, b]|) + ( - (s * |[a, b]|))) + (s * p2))) by RLVECT_1:def 3

 .= ((((1 - s) * p1) + (( - 1) * |[a, b]|)) + (((s * |[a, b]|) + (( - s) * |[a, b]|)) + (s * p2))) by RLVECT_1: 79

 .= ((((1 - s) * p1) + (( - 1) * |[a, b]|)) + (((s + ( - s)) * |[a, b]|) + (s * p2))) by RLVECT_1:def 6

 .= ((((1 - s) * p1) + (( - 1) * |[a, b]|)) + (( 0. ( TOP-REAL 2)) + (s * p2))) by RLVECT_1: 10

 .= ((((1 - s) * p1) + (( - 1) * |[a, b]|)) + (s * p2)) by RLVECT_1: 4

 .= ((((1 - s) * p1) + (s * p2)) + (( - 1) * |[a, b]|)) by RLVECT_1:def 3;



 then

 A12: p = (((((1 - s) * p1) + (s * p2)) + (( - 1) * |[a, b]|)) + |[a, b]|)

 .= (((((1 - s) * p1) + (s * p2)) + ( - |[a, b]|)) + |[a, b]|)

 .= ((((1 - s) * p1) + (s * p2)) + (( - |[a, b]|) + |[a, b]|)) by RLVECT_1:def 3

 .= ((((1 - s) * p1) + (s * p2)) + ( 0. ( TOP-REAL 2))) by RLVECT_1: 5

 .= (((1 - s) * p1) + (s * p2)) by RLVECT_1: 4;

 r = |.(p9 + ( 0. ( TOP-REAL 2))).| by A9, RLVECT_1: 4

 .= |.(p9 + ( |[a, b]| - |[a, b]|)).| by RLVECT_1: 5

 .= |.((p9 + |[a, b]|) + ( - |[a, b]|)).| by RLVECT_1:def 3

 .= |.(p - |[a, b]|).|;

 then p in { p99 where p99 be Point of ( TOP-REAL 2) : |.(p99 - |[a, b]|).| = r };

 then

 A13: p in ( circle (a,b,r)) by JGRAPH_6:def 5;

 (((1 - s) * p1) + (s * p2)) in ( LSeg (p1,p2)) by A11;

 hence thesis by A12, A13, XBOOLE_0:def 4;

 end;

 theorem :: EUCLID_6:11



 Th11: ( angle (p1,p,p2)) = PI implies p in ( LSeg (p1,p2))

 proof

 assume

 A1: ( angle (p1,p,p2)) = PI ;

 set r = |.(p - p1).|;

 set b = (p1 `2 );

 set a = (p1 `1 );



 A2: p1 = |[a, b]| by EUCLID: 53;

 per cases ;

 suppose p = p1 or p = p2;

 hence thesis by RLTOPSP1: 68;

 end;

 suppose

 A3: p <> p1 & p <> p2;



 A4: ( |.(p2 - p1).| ^2 ) = ((( |.(p1 - p).| ^2 ) + ( |.(p2 - p).| ^2 )) - (((2 * |.(p1 - p).|) * |.(p2 - p).|) * ( - 1))) by A1, Th7, SIN_COS: 77

 .= (( |.(p1 - p).| + |.(p2 - p).|) ^2 );

 |.(p2 - p1).| > r

 proof

 assume |.(p2 - p1).| <= r;

 then ( |.(p2 - p1).| ^2 ) <= (r ^2 ) by SQUARE_1: 15;

 then ((r + |.(p2 - p).|) ^2 ) <= (r ^2 ) by A4, Lm2;

 then ((((r ^2 ) + ((2 * r) * |.(p2 - p).|)) + ( |.(p2 - p).| ^2 )) - (r ^2 )) <= ((r ^2 ) - (r ^2 )) by XREAL_1: 9;

 then

 A5: (((2 * r) + |.(p2 - p).|) * |.(p2 - p).|) <= 0 ;

 |.(p2 - p).| <> 0 by A3, Lm1;

 hence contradiction by A5;

 end;

 then p2 in { p4 : |.(p4 - |[a, b]|).| > r } by A2;

 then

 A6: p2 in ( outside_of_circle (a,b,r)) by JGRAPH_6:def 8;



 A7: |.(p1 - |[a, b]|).| = 0 by A2, Lm1;

 r <> 0 by A3, Lm1;

 then p1 in { p4 : |.(p4 - |[a, b]|).| < r } by A7;

 then p1 in ( inside_of_circle (a,b,r)) by JGRAPH_6:def 6;

 then

 consider p3 such that

 A8: p3 in (( LSeg (p1,p2)) /\ ( circle (a,b,r))) by A6, Lm17;



 A9: ( euc2cpx p1) <> ( euc2cpx p2) by A1, COMPLEX2: 79;



 A10: ( euc2cpx p) <> ( euc2cpx p1) & ( euc2cpx p) <> ( euc2cpx p2) by A3, EUCLID_3: 4;



 A11: ( angle (p,p1,p2)) = 0

 proof

 assume ( angle (p,p1,p2)) <> 0 ;

 then

 A12: ( angle (p,p1,p2)) > 0 by COMPLEX2: 70;



 A13: ( angle (p,p1,p2)) < (2 * PI ) by COMPLEX2: 70;

 per cases by A10, A9, COMPLEX2: 88;

 suppose

 A14: ((( angle (p,p1,p2)) + ( angle (p1,p2,p))) + ( angle (p2,p,p1))) = PI ;



 A15: ( angle (p1,p2,p)) >= 0 by COMPLEX2: 70;

 ((( angle (p,p1,p2)) + ( angle (p1,p2,p))) + PI ) = PI by A1, A14, COMPLEX2: 82;

 hence contradiction by A12, A15;

 end;

 suppose

 A16: ((( angle (p,p1,p2)) + ( angle (p1,p2,p))) + ( angle (p2,p,p1))) = (5 * PI );

 ( angle (p1,p2,p)) < (2 * PI ) by COMPLEX2: 70;

 then

 A17: (( angle (p,p1,p2)) + ( angle (p1,p2,p))) < ((2 * PI ) + (2 * PI )) by A13, XREAL_1: 8;

 ((( angle (p,p1,p2)) + ( angle (p1,p2,p))) + PI ) = (5 * PI ) by A1, A16, COMPLEX2: 82;

 hence contradiction by A17;

 end;

 end;

 p3 in ( circle (a,b,r)) by A8, XBOOLE_0:def 4;

 then p3 in { p4 : |.(p4 - |[a, b]|).| = r } by JGRAPH_6:def 5;

 then

 A18: ex p4 st p3 = p4 & |.(p4 - |[a, b]|).| = r;

 then

 A19: |.(p3 - p1).| = r by EUCLID: 53;

 r <> 0 by A3, Lm1;

 then

 A20: p3 <> p1 by A2, A18, Lm1;



 A21: p3 in ( LSeg (p1,p2)) by A8, XBOOLE_0:def 4;

 ( |.(p3 - p).| ^2 ) = ((( |.(p - p1).| ^2 ) + ( |.(p3 - p1).| ^2 )) - (((2 * |.(p - p1).|) * |.(p3 - p1).|) * ( cos ( angle (p,p1,p3))))) by Th7

 .= (((r ^2 ) + (r ^2 )) - (((2 * r) * r) * ( cos 0 ))) by A21, A19, A20, A11, Th10

 .= 0 by SIN_COS: 31;

 then |.(p3 - p).| = 0 ;

 hence thesis by A21, Lm1;

 end;

 end;

 theorem :: EUCLID_6:12



 Th12: p in ( LSeg (p1,p3)) & p in ( LSeg (p1,p4)) & p3 <> p4 & p <> p1 implies p3 in ( LSeg (p1,p4)) or p4 in ( LSeg (p1,p3))

 proof

 assume p in ( LSeg (p1,p3));

 then

 consider l1 be Real such that

 A1: p = (((1 - l1) * p1) + (l1 * p3)) and

 A2: 0 <= l1 and l1 <= 1;

 assume p in ( LSeg (p1,p4));

 then

 consider l2 be Real such that

 A3: p = (((1 - l2) * p1) + (l2 * p4)) and

 A4: 0 <= l2 and l2 <= 1;

 (((1 + ( - l1)) * p1) + (l1 * p3)) = (((1 + ( - l2)) * p1) + (l2 * p4)) by A1, A3;

 then (((1 * p1) + (( - l1) * p1)) + (l1 * p3)) = (((1 + ( - l2)) * p1) + (l2 * p4)) by RLVECT_1:def 6;

 then (((1 * p1) + (( - l1) * p1)) + (l1 * p3)) = (((1 * p1) + (( - l2) * p1)) + (l2 * p4)) by RLVECT_1:def 6;

 then ((p1 + (( - l1) * p1)) + (l1 * p3)) = (((1 * p1) + (( - l2) * p1)) + (l2 * p4)) by RLVECT_1:def 8;

 then ((p1 + (( - l1) * p1)) + (l1 * p3)) = ((p1 + (( - l2) * p1)) + (l2 * p4)) by RLVECT_1:def 8;

 then (( - p1) + (p1 + ((( - l1) * p1) + (l1 * p3)))) = (( - p1) + ((p1 + (( - l2) * p1)) + (l2 * p4))) by RLVECT_1:def 3;

 then ((( - p1) + p1) + ((( - l1) * p1) + (l1 * p3))) = (( - p1) + ((p1 + (( - l2) * p1)) + (l2 * p4))) by RLVECT_1:def 3;

 then (( 0. ( TOP-REAL 2)) + ((( - l1) * p1) + (l1 * p3))) = (( - p1) + ((p1 + (( - l2) * p1)) + (l2 * p4))) by RLVECT_1: 5;

 then ((( - l1) * p1) + (l1 * p3)) = (( - p1) + ((p1 + (( - l2) * p1)) + (l2 * p4))) by RLVECT_1: 4;

 then ((( - l1) * p1) + (l1 * p3)) = (( - p1) + (p1 + ((( - l2) * p1) + (l2 * p4)))) by RLVECT_1:def 3;

 then ((( - l1) * p1) + (l1 * p3)) = ((( - p1) + p1) + ((( - l2) * p1) + (l2 * p4))) by RLVECT_1:def 3;

 then ((( - l1) * p1) + (l1 * p3)) = (( 0. ( TOP-REAL 2)) + ((( - l2) * p1) + (l2 * p4))) by RLVECT_1: 5;

 then

 A5: ((( - l1) * p1) + (l1 * p3)) = ((( - l2) * p1) + (l2 * p4)) by RLVECT_1: 4;

 assume that

 A6: p3 <> p4 and

 A7: p <> p1;

 per cases ;

 suppose

 A8: l1 <= l2;

 per cases by A8, XXREAL_0: 1;

 suppose

 A9: l1 < l2;

 (((1 / l2) * (( - l1) * p1)) + ((1 / l2) * (l1 * p3))) = ((1 / l2) * ((( - l2) * p1) + (l2 * p4))) by A5, RLVECT_1:def 5;

 then ((((1 / l2) * ( - l1)) * p1) + ((1 / l2) * (l1 * p3))) = ((1 / l2) * ((( - l2) * p1) + (l2 * p4))) by RLVECT_1:def 7;

 then (((( - 1) * ((1 / l2) * l1)) * p1) + (((1 / l2) * l1) * p3)) = ((1 / l2) * ((( - l2) * p1) + (l2 * p4))) by RLVECT_1:def 7;

 then (((( - 1) * ((l1 / l2) * 1)) * p1) + (((1 / l2) * l1) * p3)) = ((1 / l2) * ((( - l2) * p1) + (l2 * p4))) by XCMPLX_1: 75;

 then ((( - (l1 / l2)) * p1) + (((l1 / l2) * 1) * p3)) = ((1 / l2) * ((( - l2) * p1) + (l2 * p4))) by XCMPLX_1: 75;

 then ((( - (l1 / l2)) * p1) + ((l1 / l2) * p3)) = (((1 / l2) * (( - l2) * p1)) + ((1 / l2) * (l2 * p4))) by RLVECT_1:def 5;

 then ((( - (l1 / l2)) * p1) + ((l1 / l2) * p3)) = ((((1 / l2) * ( - l2)) * p1) + ((1 / l2) * (l2 * p4))) by RLVECT_1:def 7;

 then ((( - (l1 / l2)) * p1) + ((l1 / l2) * p3)) = (((( - 1) * ((1 / l2) * l2)) * p1) + (((1 / l2) * l2) * p4)) by RLVECT_1:def 7;

 then ((( - (l1 / l2)) * p1) + ((l1 / l2) * p3)) = (((( - 1) * ((l2 / l2) * 1)) * p1) + (((1 / l2) * l2) * p4)) by XCMPLX_1: 75;

 then ((( - (l1 / l2)) * p1) + ((l1 / l2) * p3)) = (((( - 1) * (l2 / l2)) * p1) + (((l2 / l2) * 1) * p4)) by XCMPLX_1: 75;

 then ((( - (l1 / l2)) * p1) + ((l1 / l2) * p3)) = (((( - 1) * 1) * p1) + ((l2 / l2) * p4)) by A2, A9, XCMPLX_1: 60;

 then ((( - (l1 / l2)) * p1) + ((l1 / l2) * p3)) = ((( - 1) * p1) + (1 * p4)) by A2, A9, XCMPLX_1: 60;

 then ((( - (l1 / l2)) * p1) + ((l1 / l2) * p3)) = (( - p1) + (1 * p4));

 then

 A10: ((( - (l1 / l2)) * p1) + ((l1 / l2) * p3)) = (p4 + ( - p1)) by RLVECT_1:def 8;

 (l1 / l2) < (l2 / l2) by A2, A9, XREAL_1: 74;

 then

 A11: (l1 / l2) < 1 by A2, A9, XCMPLX_1: 60;

 p4 = ((p4 - p1) + p1) by RLVECT_4: 1

 .= ((p1 + (( - (l1 / l2)) * p1)) + ((l1 / l2) * p3)) by A10, RLVECT_1:def 3

 .= (((1 * p1) + (( - (l1 / l2)) * p1)) + ((l1 / l2) * p3)) by RLVECT_1:def 8

 .= (((1 + ( - (l1 / l2))) * p1) + ((l1 / l2) * p3)) by RLVECT_1:def 6

 .= (((1 - (l1 / l2)) * p1) + ((l1 / l2) * p3));

 hence thesis by A2, A4, A11;

 end;

 suppose l1 = l2;

 then (((l1 * p1) + (( - l1) * p1)) + (l1 * p3)) = ((l1 * p1) + ((( - l1) * p1) + (l1 * p4))) by A5, RLVECT_1:def 3;

 then (((l1 + ( - l1)) * p1) + (l1 * p3)) = ((l1 * p1) + ((( - l1) * p1) + (l1 * p4))) by RLVECT_1:def 6;

 then (( 0. ( TOP-REAL 2)) + (l1 * p3)) = ((l1 * p1) + ((( - l1) * p1) + (l1 * p4))) by RLVECT_1: 10;

 then (l1 * p3) = ((l1 * p1) + ((( - l1) * p1) + (l1 * p4))) by RLVECT_1: 4;

 then (l1 * p3) = (((l1 * p1) + (( - l1) * p1)) + (l1 * p4)) by RLVECT_1:def 3;

 then (l1 * p3) = (((l1 + ( - l1)) * p1) + (l1 * p4)) by RLVECT_1:def 6;

 then (l1 * p3) = (( 0. ( TOP-REAL 2)) + (l1 * p4)) by RLVECT_1: 10;

 then

 A12: (l1 * p3) = (l1 * p4) by RLVECT_1: 4;

 per cases by A12, RLVECT_1: 36;

 suppose l1 = 0 ;



 then p = (p1 + ( 0 qua Real * p3)) by A1, RLVECT_1:def 8

 .= (p1 + ( 0. ( TOP-REAL 2))) by RLVECT_1: 10

 .= p1 by RLVECT_1: 4;

 hence thesis by A7;

 end;

 suppose p3 = p4;

 hence thesis by A6;

 end;

 end;

 end;

 suppose

 A13: l1 > l2;

 (((1 / l1) * (( - l1) * p1)) + ((1 / l1) * (l1 * p3))) = ((1 / l1) * ((( - l2) * p1) + (l2 * p4))) by A5, RLVECT_1:def 5;

 then ((((1 / l1) * ( - l1)) * p1) + ((1 / l1) * (l1 * p3))) = ((1 / l1) * ((( - l2) * p1) + (l2 * p4))) by RLVECT_1:def 7;

 then (((( - 1) * ((1 / l1) * l1)) * p1) + (((1 / l1) * l1) * p3)) = ((1 / l1) * ((( - l2) * p1) + (l2 * p4))) by RLVECT_1:def 7;

 then (((( - 1) * ((l1 / l1) * 1)) * p1) + (((1 / l1) * l1) * p3)) = ((1 / l1) * ((( - l2) * p1) + (l2 * p4))) by XCMPLX_1: 75;

 then ((( - (l1 / l1)) * p1) + (((l1 / l1) * 1) * p3)) = ((1 / l1) * ((( - l2) * p1) + (l2 * p4))) by XCMPLX_1: 75;

 then ((( - 1) * p1) + (((l1 / l1) * 1) * p3)) = ((1 / l1) * ((( - l2) * p1) + (l2 * p4))) by A4, A13, XCMPLX_1: 60;

 then ((1 * p3) + (( - 1) * p1)) = ((1 / l1) * ((( - l2) * p1) + (l2 * p4))) by A4, A13, XCMPLX_1: 60;

 then ((1 * p3) + ( - p1)) = ((1 / l1) * ((( - l2) * p1) + (l2 * p4)));

 then (p3 + ( - p1)) = ((1 / l1) * ((( - l2) * p1) + (l2 * p4))) by RLVECT_1:def 8;

 then (p3 - p1) = (((1 / l1) * (( - l2) * p1)) + ((1 / l1) * (l2 * p4))) by RLVECT_1:def 5;

 then (p3 - p1) = ((((1 / l1) * ( - l2)) * p1) + ((1 / l1) * (l2 * p4))) by RLVECT_1:def 7;

 then (p3 - p1) = (((( - 1) * ((1 / l1) * l2)) * p1) + (((1 / l1) * l2) * p4)) by RLVECT_1:def 7;

 then

 A14: (p3 - p1) = (((( - 1) * ((l2 / l1) * 1)) * p1) + (((1 / l1) * l2) * p4)) by XCMPLX_1: 75;

 (l2 / l1) < (l1 / l1) by A4, A13, XREAL_1: 74;

 then

 A15: (l2 / l1) < 1 by A4, A13, XCMPLX_1: 60;

 p3 = ((p3 - p1) + p1) by RLVECT_4: 1

 .= (((( - (l2 / l1)) * p1) + ((l2 / l1) * p4)) + p1) by A14, XCMPLX_1: 75

 .= ((p1 + (( - (l2 / l1)) * p1)) + ((l2 / l1) * p4)) by RLVECT_1:def 3

 .= (((1 * p1) + (( - (l2 / l1)) * p1)) + ((l2 / l1) * p4)) by RLVECT_1:def 8

 .= (((1 + ( - (l2 / l1))) * p1) + ((l2 / l1) * p4)) by RLVECT_1:def 6

 .= (((1 - (l2 / l1)) * p1) + ((l2 / l1) * p4));

 hence thesis by A2, A4, A15;

 end;

 end;

 theorem :: EUCLID_6:13



 Th13: p in ( LSeg (p1,p3)) & p <> p1 & p <> p3 implies (( angle (p1,p,p2)) + ( angle (p2,p,p3))) = PI or (( angle (p1,p,p2)) + ( angle (p2,p,p3))) = (3 * PI )

 proof

 assume p in ( LSeg (p1,p3)) & p <> p1 & p <> p3;

 then

 A1: ( angle (p1,p,p3)) = PI by Th8;

 (( angle (p1,p,p2)) + ( angle (p2,p,p3))) = ( angle (p1,p,p3)) or (( angle (p1,p,p2)) + ( angle (p2,p,p3))) = (( angle (p1,p,p3)) + (2 * PI )) by Th4;

 hence thesis by A1;

 end;

 theorem :: EUCLID_6:14



 Th14: p in ( LSeg (p1,p2)) & p <> p1 & p <> p2 & (( angle (p3,p,p1)) = ( PI / 2) or ( angle (p3,p,p1)) = ((3 / 2) * PI )) implies ( angle (p1,p,p3)) = ( angle (p3,p,p2))

 proof

 assume

 A1: p in ( LSeg (p1,p2)) & p <> p1 & p <> p2;

 assume

 A2: ( angle (p3,p,p1)) = ( PI / 2) or ( angle (p3,p,p1)) = ((3 / 2) * PI );



 A3: ( angle (p3,p,p1)) = ( angle (p2,p,p3))

 proof

 per cases by A1, A2, Th13;

 suppose (( angle (p2,p,p3)) + ( angle (p3,p,p1))) = PI & ( angle (p3,p,p1)) = ( PI / 2) or (( angle (p2,p,p3)) + ( angle (p3,p,p1))) = (3 * PI ) & ( angle (p3,p,p1)) = ((3 / 2) * PI );

 hence thesis;

 end;

 suppose

 A4: (( angle (p2,p,p3)) + ( angle (p3,p,p1))) = PI & ( angle (p3,p,p1)) = ((3 / 2) * PI );

 (( - PI ) / 2) < ( 0 / 2);

 hence thesis by A4, COMPLEX2: 70;

 end;

 suppose

 A5: (( angle (p2,p,p3)) + ( angle (p3,p,p1))) = (3 * PI ) & ( angle (p3,p,p1)) = ( PI / 2);

 ( 0 + (2 * PI )) < (( PI / 2) + (2 * PI )) by XREAL_1: 6;

 hence thesis by A5, COMPLEX2: 70;

 end;

 end;

 per cases ;

 suppose

 A6: ( angle (p3,p,p1)) = 0 ;

 then ( angle (p1,p,p3)) = 0 by EUCLID_3: 36;

 hence thesis by A3, A6, EUCLID_3: 36;

 end;

 suppose

 A7: ( angle (p3,p,p1)) <> 0 ;

 then ( angle (p1,p,p3)) = ((2 * PI ) - ( angle (p3,p,p1))) by EUCLID_3: 37;

 hence thesis by A3, A7, EUCLID_3: 37;

 end;

 end;

 theorem :: EUCLID_6:15



 Th15: p in ( LSeg (p1,p3)) & p in ( LSeg (p2,p4)) & p <> p1 & p <> p2 & p <> p3 & p <> p4 implies ( angle (p1,p,p2)) = ( angle (p3,p,p4))

 proof

 assume

 A1: p in ( LSeg (p1,p3));

 assume

 A2: p in ( LSeg (p2,p4));

 assume

 A3: p <> p1;

 assume

 A4: p <> p2;

 assume

 A5: p <> p3;

 assume

 A6: p <> p4;

 per cases by A1, A2, A3, A4, A5, A6, Th13;

 suppose (( angle (p1,p,p2)) + ( angle (p2,p,p3))) = PI & (( angle (p2,p,p3)) + ( angle (p3,p,p4))) = PI ;

 hence thesis;

 end;

 suppose

 A7: (( angle (p1,p,p2)) + ( angle (p2,p,p3))) = (3 * PI ) & (( angle (p2,p,p3)) + ( angle (p3,p,p4))) = PI ;

 ( angle (p3,p,p4)) >= 0 by COMPLEX2: 70;

 then (( angle (p3,p,p4)) + (2 * PI )) >= ( 0 + (2 * PI )) by XREAL_1: 6;

 hence thesis by A7, COMPLEX2: 70;

 end;

 suppose

 A8: (( angle (p1,p,p2)) + ( angle (p2,p,p3))) = PI & (( angle (p2,p,p3)) + ( angle (p3,p,p4))) = (3 * PI );

 ( angle (p3,p,p4)) < (2 * PI ) by COMPLEX2: 70;

 then (( angle (p3,p,p4)) - (2 * PI )) < ((2 * PI ) - (2 * PI )) by XREAL_1: 9;

 hence thesis by A8, COMPLEX2: 70;

 end;

 suppose (( angle (p1,p,p2)) + ( angle (p2,p,p3))) = (3 * PI ) & (( angle (p2,p,p3)) + ( angle (p3,p,p4))) = (3 * PI );

 hence thesis;

 end;

 end;

 theorem :: EUCLID_6:16



 Th16: |.(p3 - p1).| = |.(p2 - p3).| & p1 <> p2 implies ( angle (p3,p1,p2)) = ( angle (p1,p2,p3))

 proof

 assume

 A1: |.(p3 - p1).| = |.(p2 - p3).|;

 assume

 A2: p1 <> p2;

 per cases ;

 suppose

 A3: (p1,p2,p3) are_mutually_distinct ;

 ( |.(p3 - p1).| ^2 ) = ((( |.(p1 - p2).| ^2 ) + ( |.(p3 - p2).| ^2 )) - (((2 * |.(p1 - p2).|) * |.(p3 - p2).|) * ( cos ( angle (p1,p2,p3))))) by Th7;

 then ((( |.(p1 - p2).| ^2 ) + ( |.(p3 - p2).| ^2 )) - (((2 * |.(p1 - p2).|) * |.(p3 - p2).|) * ( cos ( angle (p1,p2,p3))))) = ((( |.(p3 - p1).| ^2 ) + ( |.(p2 - p1).| ^2 )) - (((2 * |.(p3 - p1).|) * |.(p2 - p1).|) * ( cos ( angle (p3,p1,p2))))) by A1, Th7;

 then ((( |.(p3 - p2).| ^2 ) - (((2 * |.(p1 - p2).|) * |.(p3 - p2).|) * ( cos ( angle (p1,p2,p3))))) + ( |.(p1 - p2).| ^2 )) = ((( |.(p3 - p1).| ^2 ) - (((2 * |.(p3 - p1).|) * |.(p2 - p1).|) * ( cos ( angle (p3,p1,p2))))) + ( |.(p2 - p1).| ^2 ));

 then ((( |.(p3 - p2).| ^2 ) - (((2 * |.(p1 - p2).|) * |.(p3 - p2).|) * ( cos ( angle (p1,p2,p3))))) + ( |.(p1 - p2).| ^2 )) = ((( |.(p3 - p1).| ^2 ) - (((2 * |.(p3 - p1).|) * |.(p2 - p1).|) * ( cos ( angle (p3,p1,p2))))) + ( |.(p1 - p2).| ^2 )) by Lm2;

 then (( - (((2 * |.(p1 - p2).|) * |.(p3 - p2).|) * ( cos ( angle (p1,p2,p3))))) + ( |.(p3 - p2).| ^2 )) = (( - (((2 * |.(p2 - p3).|) * |.(p2 - p1).|) * ( cos ( angle (p3,p1,p2))))) + ( |.(p2 - p3).| ^2 )) by A1;

 then (( - (((2 * |.(p1 - p2).|) * |.(p3 - p2).|) * ( cos ( angle (p1,p2,p3))))) + ( |.(p3 - p2).| ^2 )) = (( - (((2 * |.(p2 - p3).|) * |.(p2 - p1).|) * ( cos ( angle (p3,p1,p2))))) + ( |.(p3 - p2).| ^2 )) by Lm2;

 then (( |.(p1 - p2).| * |.(p3 - p2).|) * ( cos ( angle (p1,p2,p3)))) = (( |.(p2 - p3).| * |.(p2 - p1).|) * ( cos ( angle (p3,p1,p2))));

 then (( |.(p1 - p2).| * |.(p3 - p2).|) * ( cos ( angle (p1,p2,p3)))) = (( |.(p2 - p3).| * |.(p1 - p2).|) * ( cos ( angle (p3,p1,p2)))) by Lm2;

 then

 A4: (( |.(p3 - p2).| * ( cos ( angle (p1,p2,p3)))) * |.(p1 - p2).|) = (( |.(p2 - p3).| * ( cos ( angle (p3,p1,p2)))) * |.(p1 - p2).|);

 p1 <> p2 by A3, ZFMISC_1:def 5;

 then |.(p1 - p2).| <> 0 by Lm1;

 then ( |.(p3 - p2).| * ( cos ( angle (p1,p2,p3)))) = ( |.(p2 - p3).| * ( cos ( angle (p3,p1,p2)))) by A4, XCMPLX_1: 5;

 then

 A5: ( |.(p2 - p3).| * ( cos ( angle (p1,p2,p3)))) = ( |.(p2 - p3).| * ( cos ( angle (p3,p1,p2)))) by Lm2;

 p1 <> p3 by A3, ZFMISC_1:def 5;

 then

 A6: |.(p3 - p1).| <> 0 by Lm1;

 ( |.(p3 - p1).| * ( sin ( angle (p3,p1,p2)))) = ( |.(p3 - p2).| * ( sin ( angle (p1,p2,p3)))) by A2, Th6

 .= ( |.(p3 - p1).| * ( sin ( angle (p1,p2,p3)))) by A1, Lm2;

 then

 A7: ( sin ( angle (p3,p1,p2))) = ( sin ( angle (p1,p2,p3))) by A6, XCMPLX_1: 5;

 p2 <> p3 by A3, ZFMISC_1:def 5;

 then |.(p2 - p3).| <> 0 by Lm1;

 then ( cos ( angle (p1,p2,p3))) = ( cos ( angle (p3,p1,p2))) by A5, XCMPLX_1: 5;

 hence thesis by A7, Th1;

 end;

 suppose

 A8: not (p1,p2,p3) are_mutually_distinct ;

 per cases by A8, ZFMISC_1:def 5;

 suppose p1 = p2;

 hence thesis by A2;

 end;

 suppose

 A9: p1 = p3;

 then |.(p2 - p3).| = 0 by A1, Lm1;

 then p2 = p3 by Lm1;

 hence thesis by A9;

 end;

 suppose

 A10: p2 = p3;

 then |.(p3 - p1).| = 0 by A1, Lm1;

 then p3 = p1 by Lm1;

 hence thesis by A10;

 end;

 end;

 end;

 theorem :: EUCLID_6:17



 Th17: for p1, p2, p3, p st p in ( LSeg (p1,p2)) & p <> p2 holds |((p3 - p), (p2 - p1))| = 0 iff |((p3 - p), (p2 - p))| = 0

 proof

 let p1, p2, p3, p;

 assume p in ( LSeg (p1,p2));

 then p in ( LSeg (p2,p1));

 then

 consider l be Real such that

 A1: p = (((1 - l) * p2) + (l * p1)) and 0 <= l and l <= 1;

 assume

 A2: p <> p2;



 A3: (p2 - p) = ((p2 - ((1 - l) * p2)) - (l * p1)) by A1, RLVECT_1: 27

 .= ((p2 - ((1 * p2) - (l * p2))) - (l * p1)) by RLVECT_1: 35

 .= ((p2 - (p2 - (l * p2))) - (l * p1)) by RLVECT_1:def 8

 .= (((p2 - p2) + (l * p2)) - (l * p1)) by RLVECT_1: 29

 .= ((( 0. ( TOP-REAL 2)) + (l * p2)) - (l * p1)) by RLVECT_1: 5

 .= ((l * p2) - (l * p1)) by RLVECT_1: 4

 .= (l * (p2 - p1)) by RLVECT_1: 34;

 hereby

 assume

 A4: |((p3 - p), (p2 - p1))| = 0 ;



 thus |((p3 - p), (p2 - p))| = (l * |((p3 - p), (p2 - p1))|) by A3, EUCLID_2: 20

 .= 0 by A4;

 end;

 assume |((p3 - p), (p2 - p))| = 0 ;

 then

 A5: (l * |((p3 - p), (p2 - p1))|) = 0 by A3, EUCLID_2: 20;

 per cases by A5;

 suppose l = 0 ;



 then p = ((1 * p2) + ( 0. ( TOP-REAL 2))) by A1, RLVECT_1: 10

 .= (1 * p2) by RLVECT_1: 4

 .= p2 by RLVECT_1:def 8;

 hence thesis by A2;

 end;

 suppose |((p3 - p), (p2 - p1))| = 0 ;

 hence thesis;

 end;

 end;

 theorem :: EUCLID_6:18



 Th18: |.(p1 - p3).| = |.(p2 - p3).| & p in ( LSeg (p1,p2)) & p <> p3 & p <> p1 & (( angle (p3,p,p1)) = ( PI / 2) or ( angle (p3,p,p1)) = ((3 / 2) * PI )) implies ( angle (p1,p3,p)) = ( angle (p,p3,p2))

 proof

 assume

 A1: |.(p1 - p3).| = |.(p2 - p3).|;

 then

 A2: |.(p3 - p1).| = |.(p2 - p3).| by Lm2;

 assume

 A3: p in ( LSeg (p1,p2));

 assume that

 A4: p <> p3 and

 A5: p <> p1;

 assume

 A6: ( angle (p3,p,p1)) = ( PI / 2) or ( angle (p3,p,p1)) = ((3 / 2) * PI );

 per cases ;

 suppose

 A7: p1 = p2;

 then ( LSeg (p1,p2)) = {p1} by RLTOPSP1: 70;

 then p = p1 by A3, TARSKI:def 1;

 hence thesis by A7;

 end;

 suppose

 A8: p1 <> p2;

 per cases ;

 suppose

 A9: p <> p2;

 p2 <> p3

 proof

 assume

 A10: p2 = p3;

 then |.(p3 - p1).| = 0 by A2, Lm1;

 hence contradiction by A8, A10, Lm1;

 end;

 then

 A11: ( euc2cpx p2) <> ( euc2cpx p3) by EUCLID_3: 4;

 p1 <> p3

 proof

 assume

 A12: p1 = p3;

 then |.(p2 - p3).| = 0 by A1, Lm1;

 hence contradiction by A8, A12, Lm1;

 end;

 then

 A13: ( euc2cpx p1) <> ( euc2cpx p3) by EUCLID_3: 4;



 A14: ( euc2cpx p) <> ( euc2cpx p1) & ( euc2cpx p) <> ( euc2cpx p3) by A4, A5, EUCLID_3: 4;



 A15: ( angle (p1,p,p3)) = ( angle (p3,p,p2)) & ( euc2cpx p) <> ( euc2cpx p2) by A3, A5, A6, A9, Th14, EUCLID_3: 4;



 A16: ( angle (p3,p1,p)) = ( angle (p3,p1,p2)) by A3, A5, Th10

 .= ( angle (p1,p2,p3)) by A2, A8, Th16

 .= ( angle (p,p2,p3)) by A3, A9, Th9;



 A17: ( angle (p,p3,p1)) = ( angle (p2,p3,p))

 proof

 per cases by A16, A14, A13, A11, A15, COMPLEX2: 88;

 suppose ((( angle (p,p2,p3)) + ( angle (p,p3,p1))) + ( angle (p3,p,p2))) = PI & ((( angle (p,p2,p3)) + ( angle (p2,p3,p))) + ( angle (p3,p,p2))) = PI or ((( angle (p,p2,p3)) + ( angle (p,p3,p1))) + ( angle (p3,p,p2))) = (5 * PI ) & ((( angle (p,p2,p3)) + ( angle (p2,p3,p))) + ( angle (p3,p,p2))) = (5 * PI );

 hence thesis;

 end;

 suppose

 A18: ((( angle (p,p2,p3)) + ( angle (p,p3,p1))) + ( angle (p3,p,p2))) = PI & ((( angle (p,p2,p3)) + ( angle (p2,p3,p))) + ( angle (p3,p,p2))) = (5 * PI );

 ( angle (p2,p3,p)) < (2 * PI ) & ( angle (p,p3,p1)) >= 0 by COMPLEX2: 70;

 then

 A19: (( angle (p2,p3,p)) - ( angle (p,p3,p1))) < ((2 * PI ) - 0 ) by XREAL_1: 14;

 (( angle (p2,p3,p)) - ( angle (p,p3,p1))) = (4 * PI ) by A18;

 hence thesis by A19, XREAL_1: 64;

 end;

 suppose

 A20: ((( angle (p,p2,p3)) + ( angle (p,p3,p1))) + ( angle (p3,p,p2))) = (5 * PI ) & ((( angle (p,p2,p3)) + ( angle (p2,p3,p))) + ( angle (p3,p,p2))) = PI ;

 ( angle (p,p3,p1)) < (2 * PI ) & ( angle (p2,p3,p)) >= 0 by COMPLEX2: 70;

 then

 A21: (( angle (p,p3,p1)) - ( angle (p2,p3,p))) < ((2 * PI ) - 0 ) by XREAL_1: 14;

 (( angle (p,p3,p1)) - ( angle (p2,p3,p))) = (4 * PI ) by A20;

 hence thesis by A21, XREAL_1: 64;

 end;

 end;

 per cases ;

 suppose

 A22: ( angle (p,p3,p1)) = 0 ;

 then ( angle (p1,p3,p)) = 0 by EUCLID_3: 36;

 hence thesis by A17, A22, EUCLID_3: 36;

 end;

 suppose

 A23: ( angle (p,p3,p1)) <> 0 ;

 then ( angle (p1,p3,p)) = ((2 * PI ) - ( angle (p,p3,p1))) by EUCLID_3: 37;

 hence thesis by A17, A23, EUCLID_3: 37;

 end;

 end;

 suppose

 A24: p = p2;



 then |.(p3 - p1).| = |.(p - p3).| by A1, Lm2

 .= |.(p3 - p).| by Lm2;

 then (( |.(p3 - p1).| ^2 ) + ( |.(p1 - p).| ^2 )) = ( |.(p3 - p1).| ^2 ) by A4, A5, A6, EUCLID_3: 46;

 then |.(p1 - p).| = 0 ;

 hence thesis by A24, Lm1;

 end;

 end;

 end;

 ::$Notion-Name

 theorem :: EUCLID_6:19

 for p1, p2, p3, p st |.(p1 - p3).| = |.(p2 - p3).| & p in ( LSeg (p1,p2)) & p <> p3 holds (( angle (p1,p3,p)) = ( angle (p,p3,p2)) implies |.(p1 - p).| = |.(p - p2).|) & ( |.(p1 - p).| = |.(p - p2).| implies |((p3 - p), (p2 - p1))| = 0 ) & ( |((p3 - p), (p2 - p1))| = 0 implies ( angle (p1,p3,p)) = ( angle (p,p3,p2)))

 proof

 let p1, p2, p3, p;

 assume

 A1: |.(p1 - p3).| = |.(p2 - p3).|;

 assume

 A2: p in ( LSeg (p1,p2));

 assume

 A3: p <> p3;

 thus ( angle (p1,p3,p)) = ( angle (p,p3,p2)) implies |.(p1 - p).| = |.(p - p2).|

 proof

 assume

 A4: ( angle (p1,p3,p)) = ( angle (p,p3,p2));



 A5: ( |.(p - p1).| ^2 ) = ((( |.(p1 - p3).| ^2 ) + ( |.(p - p3).| ^2 )) - (((2 * |.(p1 - p3).|) * |.(p - p3).|) * ( cos ( angle (p1,p3,p))))) by Th7

 .= ((( |.(p - p3).| ^2 ) + ( |.(p2 - p3).| ^2 )) - (((2 * |.(p - p3).|) * |.(p2 - p3).|) * ( cos ( angle (p,p3,p2))))) by A1, A4

 .= ( |.(p2 - p).| ^2 ) by Th7;



 thus |.(p1 - p).| = |.(p - p1).| by Lm2

 .= ( sqrt ( |.(p2 - p).| ^2 )) by A5, SQUARE_1: 22

 .= |.(p2 - p).| by SQUARE_1: 22

 .= |.(p - p2).| by Lm2;

 end;

 thus |.(p1 - p).| = |.(p - p2).| implies |((p3 - p), (p2 - p1))| = 0

 proof

 assume

 A6: |.(p1 - p).| = |.(p - p2).|;

 per cases ;

 suppose

 A7: p = p2;

 then |.(p1 - p).| = 0 by A6, Lm1;



 hence |((p3 - p), (p2 - p1))| = |((p3 - p), (p - p))| by A7, Lm1

 .= |((p3 - p), ( 0. ( TOP-REAL 2)))| by RLVECT_1: 5

 .= 0 by EUCLID_2: 32;

 end;

 suppose

 A8: p <> p2;

 then |.(p1 - p).| <> 0 by A6, Lm1;

 then

 A9: p <> p1 by Lm1;



 A10: ( cos ( angle (p1,p,p3))) = ( - ( cos ( angle (p3,p,p2))))

 proof

 per cases by A2, A8, A9, Th13;

 suppose (( angle (p1,p,p3)) + ( angle (p3,p,p2))) = PI ;



 hence ( cos ( angle (p1,p,p3))) = ( cos ( PI + ( - ( angle (p3,p,p2)))))

 .= ( - ( cos ( - ( angle (p3,p,p2))))) by SIN_COS: 79

 .= ( - ( cos ( angle (p3,p,p2)))) by SIN_COS: 31;

 end;

 suppose (( angle (p1,p,p3)) + ( angle (p3,p,p2))) = (3 * PI );



 hence ( cos ( angle (p1,p,p3))) = ( cos (( PI - ( angle (p3,p,p2))) + (2 * PI )))

 .= ( cos ( PI + ( - ( angle (p3,p,p2))))) by SIN_COS: 79

 .= ( - ( cos ( - ( angle (p3,p,p2))))) by SIN_COS: 79

 .= ( - ( cos ( angle (p3,p,p2)))) by SIN_COS: 31;

 end;

 end;



 A11: ( |.(p3 - p1).| ^2 ) = ((( |.(p1 - p).| ^2 ) + ( |.(p3 - p).| ^2 )) - (((2 * |.(p1 - p).|) * |.(p3 - p).|) * ( cos ( angle (p1,p,p3))))) & ( |.(p2 - p3).| ^2 ) = ((( |.(p3 - p).| ^2 ) + ( |.(p2 - p).| ^2 )) - (((2 * |.(p3 - p).|) * |.(p2 - p).|) * ( cos ( angle (p3,p,p2))))) by Th7;



 A12: |.(p1 - p).| = |.(p2 - p).| by A6, Lm2;



 A13: |.(p2 - p).| <> 0 by A8, Lm1;



 A14: |.(p3 - p).| <> 0 by A3, Lm1;

 |.(p3 - p1).| = |.(p2 - p3).| by A1, Lm2;

 then (((2 * |.(p1 - p).|) * ( cos ( angle (p1,p,p3)))) * |.(p3 - p).|) = (((2 * |.(p2 - p).|) * ( cos ( angle (p3,p,p2)))) * |.(p3 - p).|) by A11, A12;

 then ((2 * ( cos ( angle (p1,p,p3)))) * |.(p2 - p).|) = ((2 * ( cos ( angle (p3,p,p2)))) * |.(p2 - p).|) by A14, A12, XCMPLX_1: 5;

 then

 A15: (2 * ( cos ( angle (p1,p,p3)))) = (2 * ( cos ( angle (p3,p,p2)))) by A13, XCMPLX_1: 5;

 0 <= ( angle (p3,p,p2)) & ( angle (p3,p,p2)) < (2 * PI ) by COMPLEX2: 70;

 then ( angle (p3,p,p2)) = ( PI / 2) or ( angle (p3,p,p2)) = ((3 / 2) * PI ) by A15, A10, COMPTRIG: 18;

 then |((p3 - p), (p2 - p))| = 0 by A3, A8, EUCLID_3: 45;

 hence thesis by A2, A8, Th17;

 end;

 end;

 thus |((p3 - p), (p2 - p1))| = 0 implies ( angle (p1,p3,p)) = ( angle (p,p3,p2))

 proof

 assume

 A16: |((p3 - p), (p2 - p1))| = 0 ;



 then

 A17: 0 = ( - |((p3 - p), (p2 - p1))|)

 .= |((p3 - p), ( - (p2 - p1)))| by EUCLID_2: 22

 .= |((p3 - p), (p1 - p2))| by RLVECT_1: 33;

 per cases ;

 suppose p2 = p & p1 = p;

 hence thesis;

 end;

 suppose

 A18: p1 <> p;

 then |((p3 - p), (p1 - p))| = 0 by A2, A17, Th17;

 then ( angle (p3,p,p1)) = ( PI / 2) or ( angle (p3,p,p1)) = ((3 / 2) * PI ) by A3, A18, EUCLID_3: 45;

 hence thesis by A1, A2, A3, A18, Th18;

 end;

 suppose

 A19: p2 <> p;

 then |((p3 - p), (p2 - p))| = 0 by A2, A16, Th17;

 then ( angle (p3,p,p2)) = ( PI / 2) or ( angle (p3,p,p2)) = ((3 / 2) * PI ) by A3, A19, EUCLID_3: 45;

 then

 A20: ( angle (p2,p3,p)) = ( angle (p,p3,p1)) by A1, A2, A3, A19, Th18;

 per cases ;

 suppose

 A21: ( angle (p2,p3,p)) = 0 ;

 then ( angle (p,p3,p2)) = 0 by EUCLID_3: 36;

 hence thesis by A20, A21, EUCLID_3: 36;

 end;

 suppose

 A22: ( angle (p2,p3,p)) <> 0 ;

 then ( angle (p,p3,p2)) = ((2 * PI ) - ( angle (p2,p3,p))) by EUCLID_3: 37;

 hence thesis by A20, A22, EUCLID_3: 37;

 end;

 end;

 end;

 end;

 definition

 let V be RealLinearSpace;

 ::$Canceled

 end

 notation

 let V be RealLinearSpace;

 let p1,p2,p3 be Element of V;

 antonym p1,p2,p3 is_a_triangle for p1,p2,p3 are_collinear ;

 end

 theorem :: EUCLID_6:20



 Th20: (p1,p2,p3) is_a_triangle iff (p1,p2,p3) are_mutually_distinct & ( angle (p1,p2,p3)) <> PI & ( angle (p2,p3,p1)) <> PI & ( angle (p3,p1,p2)) <> PI

 proof

 hereby

 assume

 A1: (p1,p2,p3) is_a_triangle ;

 then

 A2: not p2 in ( LSeg (p3,p1)) by TOPREAL9: 67;

 then

 A3: p2 <> p3 by RLTOPSP1: 68;



 A4: not p1 in ( LSeg (p2,p3)) by A1, TOPREAL9: 67;

 then p1 <> p2 & p1 <> p3 by RLTOPSP1: 68;

 hence (p1,p2,p3) are_mutually_distinct by A3, ZFMISC_1:def 5;

 not p3 in ( LSeg (p1,p2)) by A1, TOPREAL9: 67;

 hence ( angle (p1,p2,p3)) <> PI & ( angle (p2,p3,p1)) <> PI & ( angle (p3,p1,p2)) <> PI by A4, A2, Th11;

 end;

 assume

 A5: (p1,p2,p3) are_mutually_distinct ;

 then

 A6: p1 <> p2 by ZFMISC_1:def 5;

 assume

 A7: ( angle (p1,p2,p3)) <> PI ;



 A8: p1 <> p3 by A5, ZFMISC_1:def 5;



 A9: p2 <> p3 by A5, ZFMISC_1:def 5;

 assume ( angle (p2,p3,p1)) <> PI ;

 then

 A10: not p3 in ( LSeg (p2,p1)) by A8, A9, Th8;

 assume ( angle (p3,p1,p2)) <> PI ;

 then

 A11: not p1 in ( LSeg (p3,p2)) by A6, A8, Th8;

 not p2 in ( LSeg (p1,p3)) by A6, A9, A7, Th8;

 hence thesis by A10, A11, TOPREAL9: 67;

 end;



 Lm18: p3 <> p2 & p3 <> p1 & p2 <> p1 & p5 <> p6 & p5 <> p4 & p6 <> p4 & ( angle (p1,p2,p3)) <> PI & ( angle (p2,p3,p1)) <> PI & ( angle (p3,p1,p2)) <> PI & ( angle (p4,p5,p6)) <> PI & ( angle (p5,p6,p4)) <> PI & ( angle (p6,p4,p5)) <> PI & ( angle (p1,p2,p3)) = ( angle (p4,p5,p6)) & ( angle (p3,p1,p2)) = ( angle (p6,p4,p5)) implies ( |.(p3 - p2).| * |.(p4 - p6).|) = ( |.(p1 - p3).| * |.(p6 - p5).|)

 proof

 assume that

 A1: p3 <> p2 & p3 <> p1 and

 A2: p2 <> p1;



 A3: ( euc2cpx p3) <> ( euc2cpx p2) & ( euc2cpx p3) <> ( euc2cpx p1) by A1, EUCLID_3: 4;



 A4: ( euc2cpx p2) <> ( euc2cpx p1) by A2, EUCLID_3: 4;

 assume that

 A5: p5 <> p6 and

 A6: p5 <> p4 and

 A7: p6 <> p4;



 A8: ( euc2cpx p5) <> ( euc2cpx p6) & ( euc2cpx p5) <> ( euc2cpx p4) by A5, A6, EUCLID_3: 4;



 A9: ( euc2cpx p6) <> ( euc2cpx p4) by A7, EUCLID_3: 4;

 assume

 A10: ( angle (p1,p2,p3)) <> PI & ( angle (p2,p3,p1)) <> PI & ( angle (p3,p1,p2)) <> PI ;

 assume

 A11: ( angle (p4,p5,p6)) <> PI & ( angle (p5,p6,p4)) <> PI & ( angle (p6,p4,p5)) <> PI ;

 assume that

 A12: ( angle (p1,p2,p3)) = ( angle (p4,p5,p6)) and

 A13: ( angle (p3,p1,p2)) = ( angle (p6,p4,p5));



 A14: (( sin ( angle (p2,p1,p3))) * ( sin ( angle (p6,p5,p4)))) = (( sin ( angle (p2,p1,p3))) * ( - ( sin ( angle (p1,p2,p3))))) by A12, Th2

 .= (( - ( sin ( angle (p6,p4,p5)))) * ( - ( sin ( angle (p1,p2,p3))))) by A13, Th2

 .= (( sin ( angle (p5,p4,p6))) * ( - ( sin ( angle (p1,p2,p3))))) by Th2

 .= (( sin ( angle (p3,p2,p1))) * ( sin ( angle (p5,p4,p6)))) by Th2;

 per cases ;

 suppose

 A15: (( sin ( angle (p3,p2,p1))) * ( sin ( angle (p5,p4,p6)))) <> 0 ;



 A16: ((( |.(p3 - p2).| * |.(p4 - p6).|) * ( sin ( angle (p3,p2,p1)))) * ( sin ( angle (p5,p4,p6)))) = (( |.(p3 - p2).| * ( sin ( angle (p3,p2,p1)))) * ( |.(p4 - p6).| * ( sin ( angle (p5,p4,p6)))))

 .= (( |.(p3 - p1).| * ( sin ( angle (p2,p1,p3)))) * ( |.(p4 - p6).| * ( sin ( angle (p5,p4,p6))))) by A2, Th6

 .= (( |.(p3 - p1).| * ( sin ( angle (p2,p1,p3)))) * ( |.(p6 - p4).| * ( sin ( angle (p5,p4,p6))))) by Lm2

 .= (( |.(p3 - p1).| * ( sin ( angle (p2,p1,p3)))) * ( |.(p6 - p5).| * ( sin ( angle (p6,p5,p4))))) by A6, Th6

 .= ((( |.(p3 - p1).| * |.(p6 - p5).|) * ( sin ( angle (p2,p1,p3)))) * ( sin ( angle (p6,p5,p4))));



 thus ( |.(p3 - p2).| * |.(p4 - p6).|) = ((( |.(p3 - p2).| * |.(p4 - p6).|) * (( sin ( angle (p3,p2,p1))) * ( sin ( angle (p5,p4,p6))))) / (( sin ( angle (p3,p2,p1))) * ( sin ( angle (p5,p4,p6))))) by A15, XCMPLX_1: 89

 .= ((( |.(p3 - p1).| * |.(p6 - p5).|) * (( sin ( angle (p2,p1,p3))) * ( sin ( angle (p6,p5,p4))))) / (( sin ( angle (p3,p2,p1))) * ( sin ( angle (p5,p4,p6))))) by A16

 .= ( |.(p3 - p1).| * |.(p6 - p5).|) by A14, A15, XCMPLX_1: 89

 .= ( |.(p1 - p3).| * |.(p6 - p5).|) by Lm2;

 end;

 suppose

 A17: (( sin ( angle (p3,p2,p1))) * ( sin ( angle (p5,p4,p6)))) = 0 ;

 per cases by A17;

 suppose

 A18: ( sin ( angle (p3,p2,p1))) = 0 ;



 A19: ((2 * PI ) * 0 ) <= ( angle (p1,p2,p3)) & ( angle (p1,p2,p3)) < ((2 * PI ) + ((2 * PI ) * 0 )) by COMPLEX2: 70;

 ( - ( sin ( angle (p1,p2,p3)))) = 0 by A18, Th2;

 then ( angle (p1,p2,p3)) = ((2 * PI ) * 0 ) or ( angle (p1,p2,p3)) = ( PI + ((2 * PI ) * 0 )) by A19, SIN_COS6: 21;

 hence thesis by A3, A4, A10, COMPLEX2: 87;

 end;

 suppose

 A20: ( sin ( angle (p5,p4,p6))) = 0 ;



 A21: ((2 * PI ) * 0 ) <= ( angle (p6,p4,p5)) & ( angle (p6,p4,p5)) < ((2 * PI ) + ((2 * PI ) * 0 )) by COMPLEX2: 70;

 ( - ( sin ( angle (p6,p4,p5)))) = 0 by A20, Th2;

 then ( angle (p6,p4,p5)) = ((2 * PI ) * 0 ) or ( angle (p6,p4,p5)) = ( PI + ((2 * PI ) * 0 )) by A21, SIN_COS6: 21;

 hence thesis by A8, A9, A11, COMPLEX2: 87;

 end;

 end;

 end;

 theorem :: EUCLID_6:21



 Th21: (p1,p2,p3) is_a_triangle & (p4,p5,p6) is_a_triangle & ( angle (p1,p2,p3)) = ( angle (p4,p5,p6)) & ( angle (p3,p1,p2)) = ( angle (p6,p4,p5)) implies ( |.(p3 - p2).| * |.(p4 - p6).|) = ( |.(p1 - p3).| * |.(p6 - p5).|) & ( |.(p3 - p2).| * |.(p5 - p4).|) = ( |.(p2 - p1).| * |.(p6 - p5).|) & ( |.(p1 - p3).| * |.(p5 - p4).|) = ( |.(p2 - p1).| * |.(p4 - p6).|)

 proof

 assume (p1,p2,p3) is_a_triangle ;

 then

 A1: (p1,p2,p3) are_mutually_distinct by Th20;

 then

 A2: p3 <> p2 by ZFMISC_1:def 5;



 A3: p2 <> p1 by A1, ZFMISC_1:def 5;

 then

 A4: ( euc2cpx p2) <> ( euc2cpx p1) by EUCLID_3: 4;



 A5: p3 <> p1 by A1, ZFMISC_1:def 5;

 then

 A6: ( euc2cpx p3) <> ( euc2cpx p1) by EUCLID_3: 4;

 assume

 A7: (p4,p5,p6) is_a_triangle ;

 then

 A8: ( angle (p4,p5,p6)) <> PI & ( angle (p5,p6,p4)) <> PI by Th20;



 A9: (p4,p5,p6) are_mutually_distinct by A7, Th20;

 then

 A10: p5 <> p6 by ZFMISC_1:def 5;

 then

 A11: ( euc2cpx p5) <> ( euc2cpx p6) by EUCLID_3: 4;



 A12: p6 <> p4 by A9, ZFMISC_1:def 5;

 then

 A13: ( euc2cpx p6) <> ( euc2cpx p4) by EUCLID_3: 4;



 A14: p5 <> p4 by A9, ZFMISC_1:def 5;

 then

 A15: ( euc2cpx p5) <> ( euc2cpx p4) by EUCLID_3: 4;

 assume

 A16: ( angle (p1,p2,p3)) = ( angle (p4,p5,p6)) & ( angle (p3,p1,p2)) = ( angle (p6,p4,p5));



 A17: ( euc2cpx p3) <> ( euc2cpx p2) by A2, EUCLID_3: 4;



 A18: ( angle (p2,p3,p1)) = ( angle (p5,p6,p4))

 proof

 per cases by A17, A6, A4, A11, A15, A13, COMPLEX2: 88;

 suppose ((( angle (p3,p1,p2)) + ( angle (p1,p2,p3))) + ( angle (p2,p3,p1))) = PI & ((( angle (p6,p4,p5)) + ( angle (p4,p5,p6))) + ( angle (p5,p6,p4))) = PI ;

 hence thesis by A16;

 end;

 suppose ((( angle (p3,p1,p2)) + ( angle (p1,p2,p3))) + ( angle (p2,p3,p1))) = (5 * PI ) & ((( angle (p6,p4,p5)) + ( angle (p4,p5,p6))) + ( angle (p5,p6,p4))) = (5 * PI );

 hence thesis by A16;

 end;

 suppose

 A19: ((( angle (p3,p1,p2)) + ( angle (p1,p2,p3))) + ( angle (p2,p3,p1))) = PI & ((( angle (p6,p4,p5)) + ( angle (p4,p5,p6))) + ( angle (p5,p6,p4))) = (5 * PI );

 ( angle (p2,p3,p1)) >= 0 & ( - ( angle (p5,p6,p4))) > ( - (2 * PI )) by COMPLEX2: 70, XREAL_1: 24;

 then

 A20: (( angle (p2,p3,p1)) + ( - ( angle (p5,p6,p4)))) > ( 0 + ( - (2 * PI ))) by XREAL_1: 8;

 (( angle (p2,p3,p1)) - ( angle (p5,p6,p4))) = ( - (4 * PI )) by A16, A19;

 then (4 * PI ) < (2 * PI ) by A20, XREAL_1: 24;

 then ((4 * PI ) / PI ) < ((2 * PI ) / PI ) by XREAL_1: 74;

 then 4 < ((2 * PI ) / PI ) by XCMPLX_1: 89;

 then 4 < 2 by XCMPLX_1: 89;

 hence thesis;

 end;

 suppose

 A21: ((( angle (p3,p1,p2)) + ( angle (p1,p2,p3))) + ( angle (p2,p3,p1))) = (5 * PI ) & ((( angle (p6,p4,p5)) + ( angle (p4,p5,p6))) + ( angle (p5,p6,p4))) = PI ;

 ( angle (p2,p3,p1)) < (2 * PI ) & ( angle (p5,p6,p4)) >= 0 by COMPLEX2: 70;

 then (( angle (p2,p3,p1)) + ( - ( angle (p5,p6,p4)))) < ((2 * PI ) + ( - 0 )) by XREAL_1: 8;

 then ((4 * PI ) / PI ) < ((2 * PI ) / PI ) by A16, A21, XREAL_1: 74;

 then 4 < ((2 * PI ) / PI ) by XCMPLX_1: 89;

 then 4 < 2 by XCMPLX_1: 89;

 hence thesis;

 end;

 end;



 A22: ( angle (p6,p4,p5)) <> PI by A7, Th20;

 hence ( |.(p3 - p2).| * |.(p4 - p6).|) = ( |.(p1 - p3).| * |.(p6 - p5).|) by A2, A5, A3, A8, A10, A14, A12, A16, A18, Lm18;

 thus ( |.(p3 - p2).| * |.(p5 - p4).|) = ( |.(p2 - p1).| * |.(p6 - p5).|) by A2, A5, A3, A8, A22, A10, A14, A12, A16, A18, Lm18;

 thus thesis by A2, A5, A3, A8, A22, A10, A14, A12, A16, A18, Lm18;

 end;



 Lm19: p3 <> p2 & p3 <> p1 & p2 <> p1 & p4 <> p5 & p4 <> p6 & p5 <> p6 & ( angle (p1,p2,p3)) <> PI & ( angle (p2,p3,p1)) <> PI & ( angle (p3,p1,p2)) <> PI & ( angle (p4,p5,p6)) <> PI & ( angle (p5,p6,p4)) <> PI & ( angle (p6,p4,p5)) <> PI & ( angle (p1,p2,p3)) = ( angle (p4,p5,p6)) & ( angle (p3,p1,p2)) = ( angle (p5,p6,p4)) implies ( |.(p2 - p3).| * |.(p4 - p6).|) = ( |.(p3 - p1).| * |.(p5 - p4).|)

 proof

 assume that

 A1: p3 <> p2 & p3 <> p1 and

 A2: p2 <> p1;



 A3: ( euc2cpx p3) <> ( euc2cpx p2) & ( euc2cpx p3) <> ( euc2cpx p1) by A1, EUCLID_3: 4;



 A4: ( euc2cpx p2) <> ( euc2cpx p1) by A2, EUCLID_3: 4;

 assume that

 A5: p4 <> p5 & p4 <> p6 and

 A6: p5 <> p6;



 A7: ( euc2cpx p4) <> ( euc2cpx p5) & ( euc2cpx p4) <> ( euc2cpx p6) by A5, EUCLID_3: 4;



 A8: ( euc2cpx p5) <> ( euc2cpx p6) by A6, EUCLID_3: 4;

 assume

 A9: ( angle (p1,p2,p3)) <> PI & ( angle (p2,p3,p1)) <> PI & ( angle (p3,p1,p2)) <> PI ;

 assume that

 A10: ( angle (p4,p5,p6)) <> PI and

 A11: ( angle (p5,p6,p4)) <> PI and

 A12: ( angle (p6,p4,p5)) <> PI ;

 assume that

 A13: ( angle (p1,p2,p3)) = ( angle (p4,p5,p6)) and

 A14: ( angle (p3,p1,p2)) = ( angle (p5,p6,p4));



 A15: (( sin ( angle (p1,p2,p3))) * ( sin ( angle (p4,p6,p5)))) = (( sin ( angle (p4,p5,p6))) * ( - ( sin ( angle (p5,p6,p4))))) by A13, Th2

 .= (( - ( sin ( angle (p6,p5,p4)))) * ( - ( sin ( angle (p3,p1,p2))))) by A14, Th2

 .= (( sin ( angle (p6,p5,p4))) * ( sin ( angle (p3,p1,p2))));

 per cases ;

 suppose

 A16: (( sin ( angle (p1,p2,p3))) * ( sin ( angle (p4,p6,p5)))) <> 0 ;



 A17: ( |.(p4 - p5).| * ( sin ( angle (p6,p5,p4)))) = ( |.(p4 - p6).| * ( sin ( angle (p4,p6,p5)))) by A6, Th6;



 A18: ((( |.(p3 - p2).| * |.(p4 - p6).|) * ( sin ( angle (p1,p2,p3)))) * ( sin ( angle (p4,p6,p5)))) = (( |.(p3 - p2).| * ( sin ( angle (p1,p2,p3)))) * ( |.(p4 - p6).| * ( sin ( angle (p4,p6,p5)))))

 .= (( |.(p3 - p1).| * ( sin ( angle (p3,p1,p2)))) * ( |.(p4 - p5).| * ( sin ( angle (p6,p5,p4))))) by A2, A17, Th6

 .= ((( |.(p3 - p1).| * |.(p4 - p5).|) * ( sin ( angle (p6,p5,p4)))) * ( sin ( angle (p3,p1,p2))));



 thus ( |.(p2 - p3).| * |.(p4 - p6).|) = ( |.(p3 - p2).| * |.(p4 - p6).|) by Lm2

 .= ((( |.(p3 - p2).| * |.(p4 - p6).|) * (( sin ( angle (p1,p2,p3))) * ( sin ( angle (p4,p6,p5))))) / (( sin ( angle (p1,p2,p3))) * ( sin ( angle (p4,p6,p5))))) by A16, XCMPLX_1: 89

 .= ((( |.(p3 - p1).| * |.(p4 - p5).|) * (( sin ( angle (p6,p5,p4))) * ( sin ( angle (p3,p1,p2))))) / (( sin ( angle (p6,p5,p4))) * ( sin ( angle (p3,p1,p2))))) by A15, A18

 .= ( |.(p3 - p1).| * |.(p4 - p5).|) by A15, A16, XCMPLX_1: 89

 .= ( |.(p3 - p1).| * |.(p5 - p4).|) by Lm2;

 end;

 suppose

 A19: (( sin ( angle (p1,p2,p3))) * ( sin ( angle (p4,p6,p5)))) = 0 ;

 per cases by A19;

 suppose

 A20: ( sin ( angle (p1,p2,p3))) = 0 ;

 ((2 * PI ) * 0 ) <= ( angle (p1,p2,p3)) & ( angle (p1,p2,p3)) < ((2 * PI ) + ((2 * PI ) * 0 )) by COMPLEX2: 70;

 then ( angle (p1,p2,p3)) = ((2 * PI ) * 0 ) or ( angle (p1,p2,p3)) = ( PI + ((2 * PI ) * 0 )) by A20, SIN_COS6: 21;

 hence thesis by A3, A4, A9, COMPLEX2: 87;

 end;

 suppose

 A21: ( sin ( angle (p4,p6,p5))) = 0 ;

 ((2 * PI ) * 0 ) <= ( angle (p4,p6,p5)) & ( angle (p4,p6,p5)) < ((2 * PI ) + ((2 * PI ) * 0 )) by COMPLEX2: 70;

 then ( angle (p4,p6,p5)) = ((2 * PI ) * 0 ) or ( angle (p4,p6,p5)) = ( PI + ((2 * PI ) * 0 )) by A21, SIN_COS6: 21;

 then ( angle (p6,p5,p4)) = 0 & ( angle (p5,p4,p6)) = PI or ( angle (p6,p5,p4)) = PI & ( angle (p5,p4,p6)) = 0 by A7, A8, A11, COMPLEX2: 82, COMPLEX2: 87;

 hence thesis by A10, A12, COMPLEX2: 82;

 end;

 end;

 end;

 theorem :: EUCLID_6:22



 Th22: (p1,p2,p3) is_a_triangle & (p4,p5,p6) is_a_triangle & ( angle (p1,p2,p3)) = ( angle (p4,p5,p6)) & ( angle (p3,p1,p2)) = ( angle (p5,p6,p4)) implies ( |.(p2 - p3).| * |.(p4 - p6).|) = ( |.(p3 - p1).| * |.(p5 - p4).|) & ( |.(p2 - p3).| * |.(p6 - p5).|) = ( |.(p1 - p2).| * |.(p5 - p4).|) & ( |.(p3 - p1).| * |.(p6 - p5).|) = ( |.(p1 - p2).| * |.(p4 - p6).|)

 proof

 assume

 A1: (p1,p2,p3) is_a_triangle ;

 then

 A2: (p1,p2,p3) are_mutually_distinct by Th20;

 then

 A3: p3 <> p2 by ZFMISC_1:def 5;



 A4: ( angle (p3,p1,p2)) <> PI by A1, Th20;



 A5: p3 <> p1 by A2, ZFMISC_1:def 5;

 then

 A6: ( euc2cpx p3) <> ( euc2cpx p1) by EUCLID_3: 4;



 A7: p2 <> p1 by A2, ZFMISC_1:def 5;

 then

 A8: ( euc2cpx p2) <> ( euc2cpx p1) by EUCLID_3: 4;

 assume

 A9: (p4,p5,p6) is_a_triangle ;

 then

 A10: (p4,p5,p6) are_mutually_distinct by Th20;

 then

 A11: p4 <> p5 by ZFMISC_1:def 5;

 then

 A12: ( euc2cpx p4) <> ( euc2cpx p5) by EUCLID_3: 4;



 A13: p5 <> p6 by A10, ZFMISC_1:def 5;

 then

 A14: ( euc2cpx p5) <> ( euc2cpx p6) by EUCLID_3: 4;



 A15: ( angle (p6,p4,p5)) <> PI by A9, Th20;



 A16: p4 <> p6 by A10, ZFMISC_1:def 5;

 then

 A17: ( euc2cpx p4) <> ( euc2cpx p6) by EUCLID_3: 4;

 assume

 A18: ( angle (p1,p2,p3)) = ( angle (p4,p5,p6)) & ( angle (p3,p1,p2)) = ( angle (p5,p6,p4));



 A19: ( euc2cpx p3) <> ( euc2cpx p2) by A3, EUCLID_3: 4;



 A20: ( angle (p2,p3,p1)) = ( angle (p6,p4,p5))

 proof

 per cases by A19, A6, A8, A12, A17, A14, COMPLEX2: 88;

 suppose ((( angle (p3,p1,p2)) + ( angle (p1,p2,p3))) + ( angle (p2,p3,p1))) = PI & ((( angle (p5,p6,p4)) + ( angle (p6,p4,p5))) + ( angle (p4,p5,p6))) = PI ;

 hence thesis by A18;

 end;

 suppose ((( angle (p3,p1,p2)) + ( angle (p1,p2,p3))) + ( angle (p2,p3,p1))) = (5 * PI ) & ((( angle (p5,p6,p4)) + ( angle (p6,p4,p5))) + ( angle (p4,p5,p6))) = (5 * PI );

 hence thesis by A18;

 end;

 suppose

 A21: ((( angle (p3,p1,p2)) + ( angle (p1,p2,p3))) + ( angle (p2,p3,p1))) = PI & ((( angle (p5,p6,p4)) + ( angle (p6,p4,p5))) + ( angle (p4,p5,p6))) = (5 * PI );

 ( angle (p2,p3,p1)) >= 0 & ( - ( angle (p6,p4,p5))) > ( - (2 * PI )) by COMPLEX2: 70, XREAL_1: 24;

 then

 A22: (( angle (p2,p3,p1)) + ( - ( angle (p6,p4,p5)))) > ( 0 + ( - (2 * PI ))) by XREAL_1: 8;

 (( angle (p2,p3,p1)) - ( angle (p6,p4,p5))) = ( - (4 * PI )) by A18, A21;

 then (4 * PI ) < (2 * PI ) by A22, XREAL_1: 24;

 then ((4 * PI ) / PI ) < ((2 * PI ) / PI ) by XREAL_1: 74;

 then 4 < ((2 * PI ) / PI ) by XCMPLX_1: 89;

 then 4 < 2 by XCMPLX_1: 89;

 hence thesis;

 end;

 suppose

 A23: ((( angle (p3,p1,p2)) + ( angle (p1,p2,p3))) + ( angle (p2,p3,p1))) = (5 * PI ) & ((( angle (p5,p6,p4)) + ( angle (p6,p4,p5))) + ( angle (p4,p5,p6))) = PI ;

 ( angle (p2,p3,p1)) < (2 * PI ) & ( angle (p6,p4,p5)) >= 0 by COMPLEX2: 70;

 then (( angle (p2,p3,p1)) + ( - ( angle (p6,p4,p5)))) < ((2 * PI ) + ( - 0 )) by XREAL_1: 8;

 then ((4 * PI ) / PI ) < ((2 * PI ) / PI ) by A18, A23, XREAL_1: 74;

 then 4 < ((2 * PI ) / PI ) by XCMPLX_1: 89;

 then 4 < 2 by XCMPLX_1: 89;

 hence thesis;

 end;

 end;

 ( angle (p1,p2,p3)) <> PI & ( angle (p2,p3,p1)) <> PI by A1, Th20;

 hence ( |.(p2 - p3).| * |.(p4 - p6).|) = ( |.(p3 - p1).| * |.(p5 - p4).|) by A4, A3, A5, A7, A15, A11, A16, A13, A18, Lm19;



 A24: ( angle (p4,p5,p6)) <> PI & ( angle (p5,p6,p4)) <> PI by A9, Th20;

 hence ( |.(p2 - p3).| * |.(p6 - p5).|) = ( |.(p1 - p2).| * |.(p5 - p4).|) by A3, A5, A7, A15, A11, A16, A13, A18, A20, Lm19;

 thus thesis by A3, A5, A7, A24, A15, A11, A16, A13, A18, A20, Lm19;

 end;

 theorem :: EUCLID_6:23



 Th23: (p1,p2,p3) are_mutually_distinct & ( angle (p1,p2,p3)) <= PI implies ( angle (p2,p3,p1)) <= PI & ( angle (p3,p1,p2)) <= PI

 proof



 A1: ( angle (p1,p2,p3)) >= 0 by COMPLEX2: 70;

 assume

 A2: (p1,p2,p3) are_mutually_distinct ;

 then p1 <> p3 by ZFMISC_1:def 5;

 then

 A3: ( euc2cpx p1) <> ( euc2cpx p3) by EUCLID_3: 4;

 p2 <> p3 by A2, ZFMISC_1:def 5;

 then

 A4: ( euc2cpx p2) <> ( euc2cpx p3) by EUCLID_3: 4;

 p1 <> p2 by A2, ZFMISC_1:def 5;

 then ( euc2cpx p1) <> ( euc2cpx p2) by EUCLID_3: 4;

 then

 A5: ((( angle (p1,p2,p3)) + ( angle (p2,p3,p1))) + ( angle (p3,p1,p2))) = PI or ((( angle (p1,p2,p3)) + ( angle (p2,p3,p1))) + ( angle (p3,p1,p2))) = (5 * PI ) by A3, A4, COMPLEX2: 88;

 ( angle (p2,p3,p1)) < (2 * PI ) & ( angle (p3,p1,p2)) < (2 * PI ) by COMPLEX2: 70;

 then

 A6: (( angle (p2,p3,p1)) + ( angle (p3,p1,p2))) < ((2 * PI ) + (2 * PI )) by XREAL_1: 8;

 assume ( angle (p1,p2,p3)) <= PI ;

 then

 A7: (( angle (p1,p2,p3)) + (( angle (p2,p3,p1)) + ( angle (p3,p1,p2)))) < ( PI + (4 * PI )) by A6, XREAL_1: 8;



 A8: ( angle (p3,p1,p2)) >= 0 by COMPLEX2: 70;

 thus ( angle (p2,p3,p1)) <= PI

 proof

 assume ( angle (p2,p3,p1)) > PI ;

 then (( angle (p1,p2,p3)) + ( angle (p2,p3,p1))) > ( 0 + PI ) by A1, XREAL_1: 8;

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

 end;



 A9: ( angle (p2,p3,p1)) >= 0 by COMPLEX2: 70;

 thus ( angle (p3,p1,p2)) <= PI

 proof

 assume ( angle (p3,p1,p2)) > PI ;

 then (( angle (p2,p3,p1)) + ( angle (p3,p1,p2))) > ( 0 + PI ) by A9, XREAL_1: 8;

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

 end;

 end;

 theorem :: EUCLID_6:24



 Th24: (p1,p2,p3) are_mutually_distinct & ( angle (p1,p2,p3)) > PI implies ( angle (p2,p3,p1)) > PI & ( angle (p3,p1,p2)) > PI

 proof

 assume

 A1: (p1,p2,p3) are_mutually_distinct ;

 then

 A2: p1 <> p2 & p1 <> p3 by ZFMISC_1:def 5;

 assume

 A3: ( angle (p1,p2,p3)) > PI ;



 A4: p2 <> p3 by A1, ZFMISC_1:def 5;

 then (p2,p3,p1) are_mutually_distinct by A2, ZFMISC_1:def 5;

 hence ( angle (p2,p3,p1)) > PI by A3, Th23;

 (p3,p1,p2) are_mutually_distinct by A2, A4, ZFMISC_1:def 5;

 hence thesis by A3, Th23;

 end;



 Lm20: for n be Element of NAT , q1 be Point of ( TOP-REAL n) holds for f be Function of ( TOP-REAL n), R^1 st (for q be Point of ( TOP-REAL n) holds (f . q) = |.(q - q1).|) holds f is continuous

 proof

 let n be Element of NAT ;

 let q1 be Point of ( TOP-REAL n);

 let f be Function of ( TOP-REAL n), R^1 ;



 A1: the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

 then

 reconsider f1 = f as Function of ( TopSpaceMetr ( Euclid n)), ( TopSpaceMetr RealSpace ) by TOPMETR:def 6;

 assume

 A2: for q be Point of ( TOP-REAL n) holds (f . q) = |.(q - q1).|;

 now

 let r be Real, u be Element of ( Euclid n), u1 be Element of RealSpace ;

 assume that

 A3: r > 0 and

 A4: u1 = (f1 . u);

 set s1 = r;

 for w be Element of ( Euclid n), w1 be Element of RealSpace st w1 = (f1 . w) & ( dist (u,w)) < s1 holds ( dist (u1,w1)) < r

 proof

 let w be Element of ( Euclid n), w1 be Element of RealSpace ;

 assume that

 A5: w1 = (f1 . w) and

 A6: ( dist (u,w)) < s1;

 reconsider tu = u1, tw = w1 as Real;

 reconsider qw = w, qu = u as Point of ( TOP-REAL n) by TOPREAL3: 8;



 A7: ( dist (u1,w1)) = (the distance of RealSpace . (u1,w1)) by METRIC_1:def 1

 .= |.(tu - tw).| by METRIC_1:def 12, METRIC_1:def 13;



 A8: tu = |.(qu - q1).| by A2, A4;



 A9: |.((qu - q1) - (qw - q1)).| = |.((qu - q1) - (( - q1) + qw)).|

 .= |.(((qu - q1) - ( - q1)) - qw).| by RLVECT_1: 27

 .= |.(((qu + ( - q1)) + q1) - qw).|

 .= |.((qu + (q1 - q1)) - qw).| by RLVECT_1:def 3

 .= |.((qu + ( 0. ( TOP-REAL n))) - qw).| by RLVECT_1: 5

 .= |.(qu - qw).| by RLVECT_1: 4;

 w1 = |.(qw - q1).| by A2, A5;

 then ( dist (u,w)) = |.(qu - qw).| & ( dist (u1,w1)) <= |.((qu - q1) - (qw - q1)).| by A7, A8, JGRAPH_1: 28, JORDAN2C: 9;

 hence thesis by A6, A9, XXREAL_0: 2;

 end;

 hence ex s be Real st s > 0 & for w be Element of ( Euclid n), w1 be Element of RealSpace st w1 = (f1 . w) & ( dist (u,w)) < s holds ( dist (u1,w1)) < r by A3;

 end;

 then f1 is continuous by UNIFORM1: 3;

 hence f is continuous by A1, PRE_TOPC: 32, TOPMETR:def 6;

 end;



 Lm21: for n be Element of NAT , q1 be Point of ( TOP-REAL n) holds ex f be Function of ( TOP-REAL n), R^1 st (for q be Point of ( TOP-REAL n) holds (f . q) = |.(q - q1).|) & f is continuous

 proof

 let n be Element of NAT ;

 let q1 be Point of ( TOP-REAL n);

 defpred P[ object, object] means ex q be Point of ( TOP-REAL n) st q = $1 & $2 = |.(q - q1).|;



 A1: for x be object st x in the carrier of ( TOP-REAL n) holds ex y be object st P[x, y]

 proof

 let x be object;

 assume x in the carrier of ( TOP-REAL n);

 then

 reconsider q3 = x as Point of ( TOP-REAL n);

 take |.(q3 - q1).|;

 thus thesis;

 end;

 consider f1 be Function such that

 A2: ( dom f1) = the carrier of ( TOP-REAL n) & for x be object st x in the carrier of ( TOP-REAL n) holds P[x, (f1 . x)] from CLASSES1:sch 1( A1);

 ( rng f1) c= the carrier of R^1

 proof

 let z be object;

 assume z in ( rng f1);

 then

 consider xz be object such that

 A3: xz in ( dom f1) and

 A4: z = (f1 . xz) by FUNCT_1:def 3;

 consider q4 be Point of ( TOP-REAL n) such that

 A5: q4 = xz & (f1 . xz) = |.(q4 - q1).| by A2, A3;

 (f1 . xz) in REAL by A5, XREAL_0:def 1;

 hence thesis by A4, TOPMETR: 17;

 end;

 then

 reconsider f2 = f1 as Function of ( TOP-REAL n), R^1 by A2, FUNCT_2:def 1, RELSET_1: 4;



 A6: for q be Point of ( TOP-REAL n) holds (f1 . q) = |.(q - q1).|

 proof

 let q be Point of ( TOP-REAL n);

 ex q2 be Point of ( TOP-REAL n) st q2 = q & (f1 . q) = |.(q2 - q1).| by A2;

 hence thesis;

 end;

 then f2 is continuous by Lm20;

 hence thesis by A6;

 end;

 theorem :: EUCLID_6:25



 Th25: p in ( LSeg (p1,p2)) & (p1,p2,p3) is_a_triangle & ( angle (p1,p3,p2)) = ( angle (p,p3,p2)) implies p = p1

 proof

 assume

 A1: p in ( LSeg (p1,p2));

 assume

 A2: (p1,p2,p3) is_a_triangle ;

 then

 A3: ( angle (p3,p1,p2)) <> PI by Th20;



 A4: (p1,p2,p3) are_mutually_distinct by A2, Th20;

 then p1 <> p2 by ZFMISC_1:def 5;

 then

 A5: ( euc2cpx p2) <> ( euc2cpx p1) by EUCLID_3: 4;



 A6: not p3 in ( LSeg (p1,p2)) by A2, TOPREAL9: 67;

 ( not p1 in ( LSeg (p2,p3))) & not p2 in ( LSeg (p3,p1)) by A2, TOPREAL9: 67;

 then

 A7: (p1,p3,p2) is_a_triangle by A6, TOPREAL9: 67;

 p2 <> p3 by A4, ZFMISC_1:def 5;

 then

 A8: |.(p2 - p3).| <> 0 by Lm1;



 A9: p2 <> p3 by A4, ZFMISC_1:def 5;

 then

 A10: ( euc2cpx p3) <> ( euc2cpx p2) by EUCLID_3: 4;

 assume

 A11: ( angle (p1,p3,p2)) = ( angle (p,p3,p2));

 ( angle (p2,p3,p1)) <> PI by A2, Th20;

 then

 A12: ( angle (p,p3,p2)) <> PI by A11, COMPLEX2: 82;



 A13: p <> p3 by A1, A2, TOPREAL9: 67;

 then

 A14: ( euc2cpx p) <> ( euc2cpx p3) by EUCLID_3: 4;

 p1 <> p3 by A4, ZFMISC_1:def 5;

 then

 A15: ( euc2cpx p3) <> ( euc2cpx p1) by EUCLID_3: 4;



 A16: ( angle (p1,p2,p3)) <> PI by A2, Th20;



 A17: p <> p2

 proof

 assume p = p2;

 then ( angle (p1,p3,p2)) = 0 by A11, COMPLEX2: 79;

 then ( angle (p3,p2,p1)) = 0 & ( angle (p2,p1,p3)) = PI or ( angle (p3,p2,p1)) = PI & ( angle (p2,p1,p3)) = 0 by A10, A15, A5, COMPLEX2: 87;

 hence contradiction by A16, A3, COMPLEX2: 82;

 end;

 then

 A18: ( angle (p3,p2,p1)) = ( angle (p3,p2,p)) by A1, Th10;

 then

 A19: ( angle (p3,p2,p)) <> PI by A16, COMPLEX2: 82;



 A20: (p,p3,p2) are_mutually_distinct by A9, A17, A13, ZFMISC_1:def 5;



 A21: ( euc2cpx p) <> ( euc2cpx p2) by A17, EUCLID_3: 4;



 A22: ( angle (p2,p1,p3)) = ( angle (p2,p,p3))

 proof

 per cases by A10, A15, A5, A14, A21, COMPLEX2: 88;

 suppose ((( angle (p1,p3,p2)) + ( angle (p3,p2,p1))) + ( angle (p2,p1,p3))) = PI & ((( angle (p,p3,p2)) + ( angle (p3,p2,p))) + ( angle (p2,p,p3))) = PI ;

 hence thesis by A11, A18;

 end;

 suppose ((( angle (p1,p3,p2)) + ( angle (p3,p2,p1))) + ( angle (p2,p1,p3))) = (5 * PI ) & ((( angle (p,p3,p2)) + ( angle (p3,p2,p))) + ( angle (p2,p,p3))) = (5 * PI );

 hence thesis by A11, A18;

 end;

 suppose

 A23: ((( angle (p1,p3,p2)) + ( angle (p3,p2,p1))) + ( angle (p2,p1,p3))) = PI & ((( angle (p,p3,p2)) + ( angle (p3,p2,p))) + ( angle (p2,p,p3))) = (5 * PI );

 ( angle (p2,p1,p3)) >= 0 & ( - ( angle (p2,p,p3))) > ( - (2 * PI )) by COMPLEX2: 70, XREAL_1: 24;

 then

 A24: (( angle (p2,p1,p3)) + ( - ( angle (p2,p,p3)))) > ( 0 + ( - (2 * PI ))) by XREAL_1: 8;

 (( angle (p2,p1,p3)) - ( angle (p2,p,p3))) = ( - (4 * PI )) by A11, A18, A23;

 then (4 * PI ) < (2 * PI ) by A24, XREAL_1: 24;

 then ((4 * PI ) / PI ) < ((2 * PI ) / PI ) by XREAL_1: 74;

 then 4 < ((2 * PI ) / PI ) by XCMPLX_1: 89;

 then 4 < 2 by XCMPLX_1: 89;

 hence thesis;

 end;

 suppose

 A25: ((( angle (p1,p3,p2)) + ( angle (p3,p2,p1))) + ( angle (p2,p1,p3))) = (5 * PI ) & ((( angle (p,p3,p2)) + ( angle (p3,p2,p))) + ( angle (p2,p,p3))) = PI ;

 ( angle (p2,p1,p3)) < (2 * PI ) & ( angle (p2,p,p3)) >= 0 by COMPLEX2: 70;

 then (( angle (p2,p1,p3)) + ( - ( angle (p2,p,p3)))) < ((2 * PI ) + ( - 0 )) by XREAL_1: 8;

 then ((4 * PI ) / PI ) < ((2 * PI ) / PI ) by A11, A18, A25, XREAL_1: 74;

 then 4 < ((2 * PI ) / PI ) by XCMPLX_1: 89;

 then 4 < 2 by XCMPLX_1: 89;

 hence thesis;

 end;

 end;

 then ( angle (p2,p,p3)) <> PI by A3, COMPLEX2: 82;

 then (p,p3,p2) is_a_triangle by A20, A12, A19, Th20;

 then ( |.(p2 - p3).| * |.(p - p2).|) = ( |.(p1 - p2).| * |.(p2 - p3).|) by A7, A11, A22, Th21;

 then |.(p - p2).| = |.(p1 - p2).| by A8, XCMPLX_1: 5;



 then

 A26: |.(p2 - p).| = |.(p1 - p2).| by Lm2

 .= |.(p2 - p1).| by Lm2;

 assume

 A27: p1 <> p;



 A28: ( |.(p2 - p1).| ^2 ) = ((( |.(p1 - p).| ^2 ) + ( |.(p2 - p).| ^2 )) - (((2 * |.(p1 - p).|) * |.(p2 - p).|) * ( cos ( angle (p1,p,p2))))) by Th7

 .= ((( |.(p1 - p).| ^2 ) + ( |.(p2 - p).| ^2 )) - (((2 * |.(p1 - p).|) * |.(p2 - p).|) * ( - 1))) by A1, A27, A17, Th8, SIN_COS: 77;

 per cases by A26, A28;

 suppose |.(p1 - p).| = 0 ;

 hence contradiction by A27, Lm1;

 end;

 suppose ( |.(p1 - p).| + (2 * |.(p2 - p).|)) = 0 ;

 then |.(p1 - p).| = 0 ;

 hence contradiction by A27, Lm1;

 end;

 end;

 theorem :: EUCLID_6:26



 Th26: p in ( LSeg (p1,p2)) & not p3 in ( LSeg (p1,p2)) & ( angle (p1,p3,p2)) <= PI implies ( angle (p,p3,p2)) <= ( angle (p1,p3,p2))

 proof

 assume

 A1: p in ( LSeg (p1,p2));

 assume

 A2: not p3 in ( LSeg (p1,p2));

 assume

 A3: ( angle (p1,p3,p2)) <= PI ;

 assume

 A4: ( angle (p,p3,p2)) > ( angle (p1,p3,p2));

 per cases ;

 suppose p = p1;

 hence contradiction by A4;

 end;

 suppose p = p2;

 then ( angle (p,p3,p2)) = 0 by COMPLEX2: 79;

 hence contradiction by A4, COMPLEX2: 70;

 end;

 suppose

 A5: p1 = p2;

 then p in {p2} by A1, RLTOPSP1: 70;

 hence contradiction by A4, A5, TARSKI:def 1;

 end;

 suppose

 A6: p <> p2 & p1 <> p2 & p <> p1;

 then

 A7: ( euc2cpx p) <> ( euc2cpx p1) by EUCLID_3: 4;



 A8: p3 <> p1 by A2, RLTOPSP1: 68;

 then

 A9: ( euc2cpx p3) <> ( euc2cpx p1) by EUCLID_3: 4;



 A10: ( euc2cpx p2) <> ( euc2cpx p1) & ( euc2cpx p) <> ( euc2cpx p2) by A6, EUCLID_3: 4;



 A11: ( euc2cpx p) <> ( euc2cpx p3) by A1, A2, EUCLID_3: 4;



 A12: ( angle (p3,p2,p1)) = ( angle (p3,p2,p)) by A1, A6, Th10;



 A13: p3 <> p2 by A2, RLTOPSP1: 68;

 then

 A14: ( euc2cpx p3) <> ( euc2cpx p2) by EUCLID_3: 4;

 (( angle (p1,p3,p2)) + ( angle (p2,p1,p3))) = (( angle (p,p3,p2)) + ( angle (p2,p,p3)))

 proof

 per cases by A14, A9, A11, A10, COMPLEX2: 88;

 suppose ((( angle (p1,p3,p2)) + ( angle (p3,p2,p1))) + ( angle (p2,p1,p3))) = PI & ((( angle (p,p3,p2)) + ( angle (p3,p2,p))) + ( angle (p2,p,p3))) = PI ;

 hence thesis by A12;

 end;

 suppose ((( angle (p1,p3,p2)) + ( angle (p3,p2,p1))) + ( angle (p2,p1,p3))) = (5 * PI ) & ((( angle (p,p3,p2)) + ( angle (p3,p2,p))) + ( angle (p2,p,p3))) = (5 * PI );

 hence thesis by A12;

 end;

 suppose

 A15: ((( angle (p1,p3,p2)) + ( angle (p3,p2,p1))) + ( angle (p2,p1,p3))) = PI & ((( angle (p,p3,p2)) + ( angle (p3,p2,p))) + ( angle (p2,p,p3))) = (5 * PI );



 A16: ( angle (p1,p3,p2)) >= 0 & ( angle (p2,p1,p3)) >= 0 by COMPLEX2: 70;

 ( angle (p2,p,p3)) < (2 * PI ) by COMPLEX2: 70;

 then

 A17: ( - ( angle (p2,p,p3))) > ( - (2 * PI )) by XREAL_1: 24;

 ( angle (p,p3,p2)) < (2 * PI ) by COMPLEX2: 70;

 then ( - ( angle (p,p3,p2))) > ( - (2 * PI )) by XREAL_1: 24;

 then (( - ( angle (p,p3,p2))) + ( - ( angle (p2,p,p3)))) > (( - (2 * PI )) + ( - (2 * PI ))) by A17, XREAL_1: 8;

 then ((( angle (p1,p3,p2)) + ( angle (p2,p1,p3))) + (( - ( angle (p,p3,p2))) - ( angle (p2,p,p3)))) > (( 0 + 0 ) + (( - (2 * PI )) - (2 * PI ))) by A16, XREAL_1: 8;

 hence thesis by A12, A15;

 end;

 suppose

 A18: ((( angle (p1,p3,p2)) + ( angle (p3,p2,p1))) + ( angle (p2,p1,p3))) = (5 * PI ) & ((( angle (p,p3,p2)) + ( angle (p3,p2,p))) + ( angle (p2,p,p3))) = PI ;

 ( angle (p2,p1,p3)) < (2 * PI ) & ( angle (p1,p3,p2)) < (2 * PI ) by COMPLEX2: 70;

 then

 A19: (( angle (p2,p1,p3)) + ( angle (p1,p3,p2))) < ((2 * PI ) + (2 * PI )) by XREAL_1: 8;

 ( angle (p,p3,p2)) >= 0 & ( angle (p2,p,p3)) >= 0 by COMPLEX2: 70;

 then ((( angle (p2,p1,p3)) + ( angle (p1,p3,p2))) + (( - ( angle (p,p3,p2))) - ( angle (p2,p,p3)))) < (((2 * PI ) + (2 * PI )) + ( 0 + 0 )) by A19, XREAL_1: 8;

 hence thesis by A12, A18;

 end;

 end;

 then

 A20: ( angle (p2,p1,p3)) > ( angle (p2,p,p3)) by A4, XREAL_1: 8;

 per cases by A1, A6, A9, A11, A7, Th13, COMPLEX2: 88;

 suppose (( angle (p2,p,p3)) + ( angle (p3,p,p1))) = PI & ((( angle (p3,p,p1)) + ( angle (p,p1,p3))) + ( angle (p1,p3,p))) = PI ;

 then (( angle (p1,p3,p)) + ( angle (p,p1,p3))) < ( 0 + ( angle (p,p1,p3))) by A1, A20, Th9;

 then ( angle (p1,p3,p)) < 0 by XREAL_1: 6;

 hence contradiction by COMPLEX2: 70;

 end;

 suppose

 A21: (( angle (p2,p,p3)) + ( angle (p3,p,p1))) = (3 * PI ) & ((( angle (p3,p,p1)) + ( angle (p,p1,p3))) + ( angle (p1,p3,p))) = PI ;



 A22: ( angle (p,p1,p3)) >= 0 & ( angle (p1,p3,p)) >= 0 by COMPLEX2: 70;

 ( angle (p2,p,p3)) = ((( angle (p,p1,p3)) + ( angle (p1,p3,p))) + (2 * PI )) by A21;

 then ( angle (p2,p,p3)) >= ( 0 + (2 * PI )) by A22, XREAL_1: 6;

 hence contradiction by COMPLEX2: 70;

 end;

 suppose

 A23: (( angle (p2,p,p3)) + ( angle (p3,p,p1))) = PI & ((( angle (p3,p,p1)) + ( angle (p,p1,p3))) + ( angle (p1,p3,p))) = (5 * PI );

 ( angle (p,p1,p3)) < (2 * PI ) & ( angle (p1,p3,p)) < (2 * PI ) by COMPLEX2: 70;

 then (( angle (p,p1,p3)) + ( angle (p1,p3,p))) < ((2 * PI ) + (2 * PI )) by XREAL_1: 8;

 then (( angle (p2,p,p3)) + (4 * PI )) < ( 0 + (4 * PI )) by A23;

 then ( angle (p2,p,p3)) < 0 by XREAL_1: 6;

 hence contradiction by COMPLEX2: 70;

 end;

 suppose

 A24: (( angle (p2,p,p3)) + ( angle (p3,p,p1))) = (3 * PI ) & ((( angle (p3,p,p1)) + ( angle (p,p1,p3))) + ( angle (p1,p3,p))) = (5 * PI );

 (p1,p3,p2) are_mutually_distinct by A6, A8, A13, ZFMISC_1:def 5;

 then ( angle (p2,p1,p3)) <= PI by A3, Th23;

 then

 A25: ( angle (p,p1,p3)) <= PI by A1, A6, Th9;

 (p,p1,p3) are_mutually_distinct by A1, A2, A6, A8, ZFMISC_1:def 5;

 then ( angle (p1,p3,p)) <= PI & ( angle (p3,p,p1)) <= PI by A25, Th23;

 then (( angle (p3,p,p1)) + ( angle (p1,p3,p))) <= ( PI + PI ) by XREAL_1: 7;

 then ((( angle (p3,p,p1)) + ( angle (p1,p3,p))) + ( angle (p,p1,p3))) <= ((2 * PI ) + PI ) by A25, XREAL_1: 7;

 hence contradiction by A24, XREAL_1: 68;

 end;

 end;

 end;

 theorem :: EUCLID_6:27



 Th27: p in ( LSeg (p1,p2)) & not p3 in ( LSeg (p1,p2)) & ( angle (p1,p3,p2)) > PI & p <> p2 implies ( angle (p,p3,p2)) >= ( angle (p1,p3,p2))

 proof

 assume

 A1: p in ( LSeg (p1,p2));

 assume

 A2: not p3 in ( LSeg (p1,p2));

 assume

 A3: ( angle (p1,p3,p2)) > PI ;

 assume

 A4: p <> p2;

 assume

 A5: ( angle (p,p3,p2)) < ( angle (p1,p3,p2));

 per cases ;

 suppose p = p1;

 hence contradiction by A5;

 end;

 suppose

 A6: p1 = p2;

 then p in {p2} by A1, RLTOPSP1: 70;

 hence contradiction by A5, A6, TARSKI:def 1;

 end;

 suppose

 A7: p1 <> p2 & p <> p1;

 then

 A8: ( euc2cpx p2) <> ( euc2cpx p1) by EUCLID_3: 4;



 A9: ( euc2cpx p) <> ( euc2cpx p2) by A4, EUCLID_3: 4;



 A10: ( angle (p3,p2,p1)) = ( angle (p3,p2,p)) by A1, A4, Th10;



 A11: ( euc2cpx p) <> ( euc2cpx p1) by A7, EUCLID_3: 4;



 A12: ( euc2cpx p) <> ( euc2cpx p3) by A1, A2, EUCLID_3: 4;



 A13: p3 <> p1 by A2, RLTOPSP1: 68;

 then

 A14: ( euc2cpx p3) <> ( euc2cpx p1) by EUCLID_3: 4;



 A15: p3 <> p2 by A2, RLTOPSP1: 68;

 then

 A16: ( euc2cpx p3) <> ( euc2cpx p2) by EUCLID_3: 4;

 (( angle (p1,p3,p2)) + ( angle (p2,p1,p3))) = (( angle (p,p3,p2)) + ( angle (p2,p,p3)))

 proof

 per cases by A16, A14, A8, A12, A9, COMPLEX2: 88;

 suppose ((( angle (p1,p3,p2)) + ( angle (p3,p2,p1))) + ( angle (p2,p1,p3))) = PI & ((( angle (p,p3,p2)) + ( angle (p3,p2,p))) + ( angle (p2,p,p3))) = PI ;

 hence thesis by A10;

 end;

 suppose ((( angle (p1,p3,p2)) + ( angle (p3,p2,p1))) + ( angle (p2,p1,p3))) = (5 * PI ) & ((( angle (p,p3,p2)) + ( angle (p3,p2,p))) + ( angle (p2,p,p3))) = (5 * PI );

 hence thesis by A10;

 end;

 suppose

 A17: ((( angle (p1,p3,p2)) + ( angle (p3,p2,p1))) + ( angle (p2,p1,p3))) = PI & ((( angle (p,p3,p2)) + ( angle (p3,p2,p))) + ( angle (p2,p,p3))) = (5 * PI );



 A18: ( angle (p1,p3,p2)) >= 0 & ( angle (p2,p1,p3)) >= 0 by COMPLEX2: 70;

 ( angle (p2,p,p3)) < (2 * PI ) by COMPLEX2: 70;

 then

 A19: ( - ( angle (p2,p,p3))) > ( - (2 * PI )) by XREAL_1: 24;

 ( angle (p,p3,p2)) < (2 * PI ) by COMPLEX2: 70;

 then ( - ( angle (p,p3,p2))) > ( - (2 * PI )) by XREAL_1: 24;

 then (( - ( angle (p,p3,p2))) + ( - ( angle (p2,p,p3)))) > (( - (2 * PI )) + ( - (2 * PI ))) by A19, XREAL_1: 8;

 then ((( angle (p1,p3,p2)) + ( angle (p2,p1,p3))) + (( - ( angle (p,p3,p2))) - ( angle (p2,p,p3)))) > (( 0 + 0 ) + (( - (2 * PI )) - (2 * PI ))) by A18, XREAL_1: 8;

 hence thesis by A10, A17;

 end;

 suppose

 A20: ((( angle (p1,p3,p2)) + ( angle (p3,p2,p1))) + ( angle (p2,p1,p3))) = (5 * PI ) & ((( angle (p,p3,p2)) + ( angle (p3,p2,p))) + ( angle (p2,p,p3))) = PI ;

 ( angle (p2,p1,p3)) < (2 * PI ) & ( angle (p1,p3,p2)) < (2 * PI ) by COMPLEX2: 70;

 then

 A21: (( angle (p2,p1,p3)) + ( angle (p1,p3,p2))) < ((2 * PI ) + (2 * PI )) by XREAL_1: 8;

 ( angle (p,p3,p2)) >= 0 & ( angle (p2,p,p3)) >= 0 by COMPLEX2: 70;

 then ((( angle (p2,p1,p3)) + ( angle (p1,p3,p2))) + (( - ( angle (p,p3,p2))) - ( angle (p2,p,p3)))) < (((2 * PI ) + (2 * PI )) + ( 0 + 0 )) by A21, XREAL_1: 8;

 hence thesis by A10, A20;

 end;

 end;

 then ( angle (p2,p1,p3)) < ( angle (p2,p,p3)) by A5, XREAL_1: 8;

 then

 A22: ( angle (p,p1,p3)) < ( angle (p2,p,p3)) by A1, Th9;

 per cases by A1, A4, A14, A12, A11, Th13, COMPLEX2: 88;

 suppose

 A23: (( angle (p2,p,p3)) + ( angle (p3,p,p1))) = PI & ((( angle (p3,p,p1)) + ( angle (p,p1,p3))) + ( angle (p1,p3,p))) = PI ;

 (p1,p3,p2) are_mutually_distinct by A7, A13, A15, ZFMISC_1:def 5;

 then ( angle (p2,p1,p3)) > PI by A3, Th24;

 then

 A24: ( angle (p,p1,p3)) > PI by A1, A7, Th9;

 (p,p1,p3) are_mutually_distinct by A1, A2, A7, A13, ZFMISC_1:def 5;

 then ( angle (p1,p3,p)) > PI & ( angle (p3,p,p1)) > PI by A24, Th24;

 then (( angle (p3,p,p1)) + ( angle (p1,p3,p))) > ( PI + PI ) by XREAL_1: 8;

 then

 A25: ((( angle (p3,p,p1)) + ( angle (p1,p3,p))) + ( angle (p,p1,p3))) > ((2 * PI ) + PI ) by A24, XREAL_1: 8;

 (1 * PI ) < (3 * PI ) by XREAL_1: 68;

 hence contradiction by A23, A25;

 end;

 suppose

 A26: (( angle (p2,p,p3)) + ( angle (p3,p,p1))) = (3 * PI ) & ((( angle (p3,p,p1)) + ( angle (p,p1,p3))) + ( angle (p1,p3,p))) = PI ;



 A27: ( angle (p,p1,p3)) >= 0 & ( angle (p1,p3,p)) >= 0 by COMPLEX2: 70;

 ( angle (p2,p,p3)) = ((( angle (p,p1,p3)) + ( angle (p1,p3,p))) + (2 * PI )) by A26;

 then ( angle (p2,p,p3)) >= ( 0 + (2 * PI )) by A27, XREAL_1: 6;

 hence contradiction by COMPLEX2: 70;

 end;

 suppose

 A28: (( angle (p2,p,p3)) + ( angle (p3,p,p1))) = PI & ((( angle (p3,p,p1)) + ( angle (p,p1,p3))) + ( angle (p1,p3,p))) = (5 * PI );

 ( angle (p,p1,p3)) < (2 * PI ) & ( angle (p1,p3,p)) < (2 * PI ) by COMPLEX2: 70;

 then (( angle (p,p1,p3)) + ( angle (p1,p3,p))) < ((2 * PI ) + (2 * PI )) by XREAL_1: 8;

 then (( angle (p2,p,p3)) + (4 * PI )) < ( 0 + (4 * PI )) by A28;

 then ( angle (p2,p,p3)) < 0 by XREAL_1: 6;

 hence contradiction by COMPLEX2: 70;

 end;

 suppose (( angle (p2,p,p3)) + ( angle (p3,p,p1))) = (3 * PI ) & ((( angle (p3,p,p1)) + ( angle (p,p1,p3))) + ( angle (p1,p3,p))) = (5 * PI );

 then (( angle (p2,p,p3)) + (2 * PI )) = (( angle (p,p1,p3)) + ( angle (p1,p3,p)));

 then (( angle (p2,p,p3)) + (2 * PI )) < (( angle (p2,p,p3)) + ( angle (p1,p3,p))) by A22, XREAL_1: 6;

 then (2 * PI ) < ( angle (p1,p3,p)) by XREAL_1: 6;

 hence contradiction by COMPLEX2: 70;

 end;

 end;

 end;

 theorem :: EUCLID_6:28



 Th28: p in ( LSeg (p1,p2)) & not p3 in ( LSeg (p1,p2)) implies ex p4 st p4 in ( LSeg (p1,p2)) & ( angle (p1,p3,p4)) = ( angle (p,p3,p2))

 proof

 assume

 A1: p in ( LSeg (p1,p2));

 assume

 A2: not p3 in ( LSeg (p1,p2));

 per cases ;

 suppose

 A3: p1 = p2;

 set p4 = p;

 take p4;

 thus p4 in ( LSeg (p1,p2)) by A1;

 ( LSeg (p1,p2)) = {p1} by A3, RLTOPSP1: 70;

 then p = p1 by A1, TARSKI:def 1;

 hence thesis by A3;

 end;

 suppose

 A4: p = p2 or p1 in ( LSeg (p2,p3));

 set p4 = p1;

 take p4;

 thus p4 in ( LSeg (p1,p2)) by RLTOPSP1: 68;

 per cases by A4;

 suppose

 A5: p = p2;



 thus ( angle (p1,p3,p4)) = 0 by COMPLEX2: 79

 .= ( angle (p,p3,p2)) by A5, COMPLEX2: 79;

 end;

 suppose

 A6: p1 in ( LSeg (p2,p3));

 p2 in ( LSeg (p3,p2)) by RLTOPSP1: 68;

 then

 A7: ( LSeg (p1,p2)) c= ( LSeg (p3,p2)) by A6, TOPREAL1: 6;



 thus ( angle (p1,p3,p4)) = 0 by COMPLEX2: 79

 .= ( angle (p2,p3,p2)) by COMPLEX2: 79

 .= ( angle (p,p3,p2)) by A1, A2, A7, Th9;

 end;

 end;

 suppose

 A8: p = p1 or p2 in ( LSeg (p1,p3));

 set p4 = p2;

 take p4;

 thus p4 in ( LSeg (p1,p2)) by RLTOPSP1: 68;

 per cases by A8;

 suppose p = p1;

 hence thesis;

 end;

 suppose

 A9: p2 in ( LSeg (p1,p3));

 p1 in ( LSeg (p1,p3)) by RLTOPSP1: 68;

 then ( LSeg (p1,p2)) c= ( LSeg (p1,p3)) by A9, TOPREAL1: 6;

 hence thesis by A1, A2, Th9;

 end;

 end;

 suppose

 A10: p1 <> p2 & p <> p1 & p <> p2 & not p1 in ( LSeg (p2,p3)) & not p2 in ( LSeg (p1,p3));

 p1 in ( LSeg (p1,p2)) by RLTOPSP1: 68;

 then

 reconsider q1 = p1 as Point of (( TOP-REAL 2) | ( LSeg (p1,p2))) by PRE_TOPC: 8;



 A11: (1 * ( - 2)) <= (( cos ( angle (p,p3,p2))) * ( - 2)) by SIN_COS6: 6, XREAL_1: 65;

 consider f1 be Function of ( TOP-REAL 2), R^1 such that

 A12: for q be Point of ( TOP-REAL 2) holds (f1 . q) = |.(q - p1).| and

 A13: f1 is continuous by Lm21;

 consider f12 be Function of ( TOP-REAL 2), R^1 such that

 A14: for q be Point of ( TOP-REAL 2), r1,r2 be Real st (f1 . q) = r1 & (f1 . q) = r2 holds (f12 . q) = (r1 * r2) and

 A15: f12 is continuous by A13, JGRAPH_2: 25;

 consider f3 be Function of ( TOP-REAL 2), R^1 such that

 A16: for q be Point of ( TOP-REAL 2) holds (f3 . q) = |.(q - p3).| and

 A17: f3 is continuous by Lm21;

 consider f32 be Function of ( TOP-REAL 2), R^1 such that

 A18: for q be Point of ( TOP-REAL 2), r1,r2 be Real st (f3 . q) = r1 & (f3 . q) = r2 holds (f32 . q) = (r1 * r2) and

 A19: f32 is continuous by A17, JGRAPH_2: 25;



 A20: ( |.(p2 - p1).| ^2 ) = ((( |.(p1 - p3).| ^2 ) + ( |.(p2 - p3).| ^2 )) - (((2 * |.(p1 - p3).|) * |.(p2 - p3).|) * ( cos ( angle (p1,p3,p2))))) by Th7;



 A21: p2 <> p3 by A2, RLTOPSP1: 68;

 then

 A22: |.(p2 - p3).| <> 0 by Lm1;

 p2 in ( LSeg (p1,p2)) by RLTOPSP1: 68;

 then

 reconsider q2 = p2 as Point of (( TOP-REAL 2) | ( LSeg (p1,p2))) by PRE_TOPC: 8;

 consider f0 be Function of (( TOP-REAL 2) | ( LSeg (p1,p2))), ( TOP-REAL 2) such that

 A23: for q be Point of (( TOP-REAL 2) | ( LSeg (p1,p2))) holds (f0 . q) = q and

 A24: f0 is continuous by JGRAPH_6: 6;

 set d = (((( |.(p2 - p).| ^2 ) - ( |.(p - p3).| ^2 )) - ( |.(p2 - p3).| ^2 )) / ( |.(p - p3).| * |.(p2 - p3).|));

 consider f2 be Function of ( TOP-REAL 2), R^1 such that

 A25: for q be Point of ( TOP-REAL 2) holds (f2 . q) = |.(p1 - p3).| and

 A26: f2 is continuous by JGRAPH_2: 20;



 A27: p1 <> p3 by A2, RLTOPSP1: 68;

 then

 A28: |.(p1 - p3).| <> 0 by Lm1;



 A29: ( cos ( angle (p,p3,p2))) <> 1

 proof



 A30: 0 <= ( angle (p,p3,p2)) & ( angle (p,p3,p2)) < (2 * PI ) by COMPLEX2: 70;

 assume ( cos ( angle (p,p3,p2))) = 1;

 then

 A31: ( angle (p,p3,p2)) = 0 by A30, COMPTRIG: 61;



 A32: ( euc2cpx p) <> ( euc2cpx p3) & ( euc2cpx p) <> ( euc2cpx p2) by A1, A2, A10, EUCLID_3: 4;



 A33: ( euc2cpx p3) <> ( euc2cpx p2) by A21, EUCLID_3: 4;

 per cases by A31, A32, A33, COMPLEX2: 87;

 suppose ( angle (p3,p2,p)) = 0 & ( angle (p2,p,p3)) = PI ;

 then p in ( LSeg (p2,p3)) by Th11;

 hence contradiction by A1, A2, A10, A27, Th12;

 end;

 suppose ( angle (p3,p2,p)) = PI & ( angle (p2,p,p3)) = 0 ;

 then ( angle (p3,p2,p1)) = PI by A1, A10, Th10;

 hence contradiction by A10, Th11;

 end;

 end;



 A34: for q be Point of (( TOP-REAL 2) | ( LSeg (p1,p2))) holds q is Point of ( TOP-REAL 2) & q in ( LSeg (p1,p2))

 proof

 let q be Point of (( TOP-REAL 2) | ( LSeg (p1,p2)));



 A35: q in the carrier of (( TOP-REAL 2) | ( LSeg (p1,p2)));

 then q in ( LSeg (p1,p2)) by PRE_TOPC: 8;

 hence q is Point of ( TOP-REAL 2);

 thus thesis by A35, PRE_TOPC: 8;

 end;

 consider f6 be Function of ( TOP-REAL 2), R^1 such that

 A36: for q be Point of ( TOP-REAL 2), r1,r2 be Real st (f2 . q) = r1 & (f3 . q) = r2 holds (f6 . q) = (r1 * r2) and

 A37: f6 is continuous by A26, A17, JGRAPH_2: 25;

 reconsider f8 = (f6 * f0) as continuous Function of (( TOP-REAL 2) | ( LSeg (p1,p2))), R^1 by A24, A37;

 consider f22 be Function of ( TOP-REAL 2), R^1 such that

 A38: for q be Point of ( TOP-REAL 2), r1,r2 be Real st (f2 . q) = r1 & (f2 . q) = r2 holds (f22 . q) = (r1 * r2) and

 A39: f22 is continuous by A26, JGRAPH_2: 25;

 consider f4 be Function of ( TOP-REAL 2), R^1 such that

 A40: for q be Point of ( TOP-REAL 2), r1,r2 be Real st (f12 . q) = r1 & (f22 . q) = r2 holds (f4 . q) = (r1 - r2) and

 A41: f4 is continuous by A15, A39, JGRAPH_2: 21;

 consider f5 be Function of ( TOP-REAL 2), R^1 such that

 A42: for q be Point of ( TOP-REAL 2), r1,r2 be Real st (f4 . q) = r1 & (f32 . q) = r2 holds (f5 . q) = (r1 - r2) and

 A43: f5 is continuous by A19, A41, JGRAPH_2: 21;



 A44: |.(p - p3).| <> 0 by A1, A2, Lm1;

 reconsider f7 = (f5 * f0) as continuous Function of (( TOP-REAL 2) | ( LSeg (p1,p2))), R^1 by A24, A43;



 A45: for q be Point of (( TOP-REAL 2) | ( LSeg (p1,p2))), q1 be Point of ( TOP-REAL 2) st q = q1 holds (f8 . q) = ( |.(p1 - p3).| * |.(q1 - p3).|)

 proof

 let q be Point of (( TOP-REAL 2) | ( LSeg (p1,p2)));

 let q1 be Point of ( TOP-REAL 2);

 ( dom f8) = the carrier of (( TOP-REAL 2) | ( LSeg (p1,p2))) by FUNCT_2:def 1;



 then

 A46: (f8 . q) = (f6 . (f0 . q)) by FUNCT_1: 12

 .= (f6 . q) by A23;

 assume

 A47: q = q1;

 then (f6 . q) = ((f2 . q) * (f3 . q)) & (f2 . q) = |.(p1 - p3).| by A25, A36;

 hence thesis by A16, A47, A46;

 end;

 for q be Point of (( TOP-REAL 2) | ( LSeg (p1,p2))) holds (f8 . q) <> 0

 proof

 let q be Point of (( TOP-REAL 2) | ( LSeg (p1,p2)));

 reconsider q1 = q as Point of ( TOP-REAL 2) by A34;



 A48: (f8 . q) = ( |.(p1 - p3).| * |.(q1 - p3).|) by A45;

 assume

 A49: (f8 . q) = 0 ;

 per cases by A48, A49;

 suppose |.(p1 - p3).| = 0 ;

 hence contradiction by A27, Lm1;

 end;

 suppose |.(q1 - p3).| = 0 ;

 then q = p3 by Lm1;

 hence contradiction by A2, A34;

 end;

 end;

 then

 consider f9 be Function of (( TOP-REAL 2) | ( LSeg (p1,p2))), R^1 such that

 A50: for q be Point of (( TOP-REAL 2) | ( LSeg (p1,p2))), r1,r2 be Real st (f7 . q) = r1 & (f8 . q) = r2 holds (f9 . q) = (r1 / r2) and

 A51: f9 is continuous by JGRAPH_2: 27;

 consider f be Function of I[01] , (( TOP-REAL 2) | ( LSeg (p1,p2))) such that

 A52: for x be Real st x in [. 0 , 1.] holds (f . x) = (((1 - x) * p1) + (x * p2)) and

 A53: f is being_homeomorphism and

 A54: (f . 0 ) = p1 and

 A55: (f . 1) = p2 by A10, JORDAN5A: 3;

 f is continuous by A53, TOPS_2:def 5;

 then

 reconsider g = (f9 * f) as continuous Function of ( Closed-Interval-TSpace ( 0 ,1)), R^1 by A51, TOPMETR: 20;



 A56: ( dom g) = [. 0 , 1.] by BORSUK_1: 40, FUNCT_2:def 1;

 set b = (g . 1);

 1 in { r where r be Real : 0 <= r & r <= 1 };

 then 1 in ( dom g) by A56, RCOMP_1:def 1;

 then

 A57: (g . 1) = (f9 . p2) by A55, FUNCT_1: 12;

 ( |.(p2 - p).| ^2 ) = ((( |.(p - p3).| ^2 ) + ( |.(p2 - p3).| ^2 )) - (((2 * |.(p - p3).|) * |.(p2 - p3).|) * ( cos ( angle (p,p3,p2))))) by Th7;



 then

 A58: d = ((( - 2) * (( |.(p - p3).| * |.(p2 - p3).|) * ( cos ( angle (p,p3,p2))))) / ( |.(p - p3).| * |.(p2 - p3).|))

 .= (( - 2) * ((( |.(p - p3).| * |.(p2 - p3).|) * ( cos ( angle (p,p3,p2)))) / ( |.(p - p3).| * |.(p2 - p3).|))) by XCMPLX_1: 74

 .= (( - 2) * ( cos ( angle (p,p3,p2)))) by A22, A44, XCMPLX_1: 89;



 A59: for q be Point of (( TOP-REAL 2) | ( LSeg (p1,p2))), q1 be Point of ( TOP-REAL 2) st q = q1 holds (f9 . q) = (((( |.(q1 - p1).| ^2 ) - ( |.(p1 - p3).| ^2 )) - ( |.(q1 - p3).| ^2 )) / ( |.(p1 - p3).| * |.(q1 - p3).|))

 proof

 let q be Point of (( TOP-REAL 2) | ( LSeg (p1,p2)));

 let q1 be Point of ( TOP-REAL 2);



 A60: q is Point of ( TOP-REAL 2) by A34;

 ( dom f7) = the carrier of (( TOP-REAL 2) | ( LSeg (p1,p2))) by FUNCT_2:def 1;



 then

 A61: (f7 . q) = (f5 . (f0 . q)) by FUNCT_1: 12

 .= (f5 . q) by A23

 .= ((f4 . q) - (f32 . q)) by A42, A60

 .= (((f12 . q) - (f22 . q)) - (f32 . q)) by A40, A60

 .= (((f12 . q) - (f22 . q)) - ((f3 . q) * (f3 . q))) by A18, A60

 .= ((((f1 . q) * (f1 . q)) - (f22 . q)) - ((f3 . q) * (f3 . q))) by A14, A60

 .= ((((f1 . q) * (f1 . q)) - ((f2 . q) * (f2 . q))) - ((f3 . q) * (f3 . q))) by A38, A60;



 A62: (f9 . q) = ((f7 . q) / (f8 . q)) by A50;

 assume

 A63: q = q1;

 then

 A64: (f3 . q) = |.(q1 - p3).| by A16;

 (f1 . q) = |.(q1 - p1).| & (f2 . q) = |.(p1 - p3).| by A12, A25, A63;

 hence thesis by A45, A63, A62, A61, A64;

 end;

 then (f9 . q2) = (((( |.(p2 - p1).| ^2 ) - ( |.(p1 - p3).| ^2 )) - ( |.(p2 - p3).| ^2 )) / ( |.(p1 - p3).| * |.(p2 - p3).|));



 then

 A65: (f9 . q2) = ((( - 2) * (( |.(p1 - p3).| * |.(p2 - p3).|) * ( cos ( angle (p1,p3,p2))))) / ( |.(p1 - p3).| * |.(p2 - p3).|)) by A20

 .= (( - 2) * ((( |.(p1 - p3).| * |.(p2 - p3).|) * ( cos ( angle (p1,p3,p2)))) / ( |.(p1 - p3).| * |.(p2 - p3).|))) by XCMPLX_1: 74

 .= (( - 2) * ( cos ( angle (p1,p3,p2)))) by A28, A22, XCMPLX_1: 89;



 A66: d < b

 proof

 per cases ;

 suppose

 A67: ( angle (p1,p3,p2)) <= PI ;



 A68: ( [. 0 , PI .] /\ ( dom cos )) = [. 0 , PI .] by SIN_COS: 24, XBOOLE_1: 28;

 0 <= ( angle (p1,p3,p2)) by COMPLEX2: 70;

 then

 A69: ( angle (p1,p3,p2)) in ( [. 0 , PI .] /\ ( dom cos )) by A67, A68, XXREAL_1: 1;



 A70: ( cos . ( angle (p1,p3,p2))) = ( cos ( angle (p1,p3,p2))) & ( cos . ( angle (p,p3,p2))) = ( cos ( angle (p,p3,p2))) by SIN_COS:def 19;



 A71: ( angle (p,p3,p2)) <= ( angle (p1,p3,p2)) by A1, A2, A67, Th26;

 then 0 <= ( angle (p,p3,p2)) & ( angle (p,p3,p2)) <= PI by A67, COMPLEX2: 70, XXREAL_0: 2;

 then

 A72: ( angle (p,p3,p2)) in ( [. 0 , PI .] /\ ( dom cos )) by A68, XXREAL_1: 1;

 (p1,p2,p3) is_a_triangle by A2, A10, TOPREAL9: 67;

 then

 A73: ( angle (p,p3,p2)) < ( angle (p1,p3,p2)) by A1, A10, A71, Th25, XXREAL_0: 1;

 ( cos | [.((2 * PI ) * 0 ), ( PI + ((2 * PI ) * 0 )).]) is decreasing by SIN_COS6: 55;

 then ( cos . ( angle (p1,p3,p2))) < ( cos . ( angle (p,p3,p2))) by A73, A72, A69, RFUNCT_2: 21;

 hence thesis by A57, A65, A58, A70, XREAL_1: 69;

 end;

 suppose

 A74: ( angle (p1,p3,p2)) > PI ;



 A75: ( [. PI , (2 * PI ).] /\ ( dom cos )) = [. PI , (2 * PI ).] by SIN_COS: 24, XBOOLE_1: 28;



 A76: ( angle (p,p3,p2)) <= (2 * PI ) by COMPLEX2: 70;



 A77: ( angle (p,p3,p2)) >= ( angle (p1,p3,p2)) by A1, A2, A10, A74, Th27;

 then PI <= ( angle (p,p3,p2)) by A74, XXREAL_0: 2;

 then

 A78: ( angle (p,p3,p2)) in ( [. PI , (2 * PI ).] /\ ( dom cos )) by A75, A76, XXREAL_1: 1;

 ( angle (p1,p3,p2)) <= (2 * PI ) by COMPLEX2: 70;

 then

 A79: ( angle (p1,p3,p2)) in ( [. PI , (2 * PI ).] /\ ( dom cos )) by A74, A75, XXREAL_1: 1;



 A80: ( cos . ( angle (p1,p3,p2))) = ( cos ( angle (p1,p3,p2))) & ( cos . ( angle (p,p3,p2))) = ( cos ( angle (p,p3,p2))) by SIN_COS:def 19;

 (p1,p2,p3) is_a_triangle by A2, A10, TOPREAL9: 67;

 then

 A81: ( angle (p,p3,p2)) > ( angle (p1,p3,p2)) by A1, A10, A77, Th25, XXREAL_0: 1;

 ( cos | [.( PI + ((2 * PI ) * 0 )), ((2 * PI ) + ((2 * PI ) * 0 )).]) is increasing by SIN_COS6: 56;

 then ( cos . ( angle (p1,p3,p2))) < ( cos . ( angle (p,p3,p2))) by A81, A78, A79, RFUNCT_2: 20;

 hence thesis by A57, A65, A58, A80, XREAL_1: 69;

 end;

 end;

 set a = (g . 0 );

 0 in { r where r be Real : 0 <= r & r <= 1 };

 then 0 in ( dom g) by A56, RCOMP_1:def 1;

 then

 A82: (g . 0 ) = (f9 . p1) by A54, FUNCT_1: 12;



 A83: (f9 . q1) = (((( |.(p1 - p1).| ^2 ) - ( |.(p1 - p3).| ^2 )) - ( |.(p1 - p3).| ^2 )) / ( |.(p1 - p3).| * |.(p1 - p3).|)) by A59

 .= (((( 0 ^2 ) - ( |.(p1 - p3).| ^2 )) - ( |.(p1 - p3).| ^2 )) / ( |.(p1 - p3).| * |.(p1 - p3).|)) by Lm1

 .= ((( - 2) * ( |.(p1 - p3).| ^2 )) / ( |.(p1 - p3).| * |.(p1 - p3).|))

 .= ( - 2) by A28, XCMPLX_1: 89;

 then a <> d by A82, A58, A29;

 then a < d by A82, A83, A58, A11, XXREAL_0: 1;

 then

 consider rc be Real such that

 A84: (g . rc) = d and

 A85: 0 < rc & rc < 1 by A66, TOPREAL5: 6;

 rc in { r where r be Real : 0 <= r & r <= 1 } by A85;

 then

 A86: rc in ( dom g) by A56, RCOMP_1:def 1;

 then

 A87: (f . rc) = (((1 - rc) * p1) + (rc * p2)) by A52, A56;

 set p4 = (((1 - rc) * p1) + (rc * p2));

 take p4;

 thus

 A88: p4 in ( LSeg (p1,p2)) by A85;

 then

 reconsider q = p4 as Point of (( TOP-REAL 2) | ( LSeg (p1,p2))) by PRE_TOPC: 8;



 A89: |.(p4 - p3).| <> 0 by A2, A88, Lm1;

 set r2 = ( |.(p1 - p3).| * |.(p4 - p3).|);



 A90: ( |.(p4 - p1).| ^2 ) = ((( |.(p1 - p3).| ^2 ) + ( |.(p4 - p3).| ^2 )) - (((2 * |.(p1 - p3).|) * |.(p4 - p3).|) * ( cos ( angle (p1,p3,p4))))) by Th7;

 (f9 . q) = (((( |.(p4 - p1).| ^2 ) - ( |.(p1 - p3).| ^2 )) - ( |.(p4 - p3).| ^2 )) / ( |.(p1 - p3).| * |.(p4 - p3).|)) by A59;



 then

 A91: d = ((( - 2) * (r2 * ( cos ( angle (p1,p3,p4))))) / r2) by A84, A86, A87, A90, FUNCT_1: 12

 .= (( - 2) * ((r2 * ( cos ( angle (p1,p3,p4)))) / r2)) by XCMPLX_1: 74

 .= (( - 2) * ( cos ( angle (p1,p3,p4)))) by A28, A89, XCMPLX_1: 89;



 A92: p1 <> p4

 proof



 A93: |.(p1 - p3).| <> 0 by A27, Lm1;

 assume

 A94: p1 = p4;

 0 = ( 0 * |.(p1 - p1).|)

 .= (((2 * |.(p1 - p3).|) * |.(p1 - p3).|) - (((2 * |.(p1 - p3).|) * |.(p1 - p3).|) * ( cos ( angle (p1,p3,p4))))) by A90, A94, Lm1;

 hence contradiction by A58, A29, A91, A93, XCMPLX_1: 7;

 end;



 A95: p3 <> p4 by A2, A85;

 per cases ;

 suppose

 A96: ( angle (p,p3,p2)) <= PI ;

 (p,p3,p2) are_mutually_distinct by A1, A2, A10, A21, ZFMISC_1:def 5;

 then ( angle (p3,p2,p)) <= PI by A96, Th23;

 then

 A97: ( angle (p3,p2,p1)) <= PI by A1, A10, Th10;

 (p3,p2,p1) are_mutually_distinct by A10, A27, A21, ZFMISC_1:def 5;

 then ( angle (p2,p1,p3)) <= PI by A97, Th23;

 then

 A98: ( angle (p4,p1,p3)) <= PI by A88, A92, Th9;

 (p4,p1,p3) are_mutually_distinct by A27, A92, A95, ZFMISC_1:def 5;

 then ( angle (p1,p3,p4)) <= PI by A98, Th23;



 hence ( angle (p1,p3,p4)) = ( arccos ( cos ( angle (p1,p3,p4)))) by COMPLEX2: 70, SIN_COS6: 92

 .= ( angle (p,p3,p2)) by A58, A91, A96, COMPLEX2: 70, SIN_COS6: 92;

 end;

 suppose

 A99: ( angle (p,p3,p2)) > PI ;

 (p,p3,p2) are_mutually_distinct by A1, A2, A10, A21, ZFMISC_1:def 5;

 then ( angle (p3,p2,p)) > PI by A99, Th24;

 then

 A100: ( angle (p3,p2,p1)) > PI by A1, A10, Th10;

 (p3,p2,p1) are_mutually_distinct by A10, A27, A21, ZFMISC_1:def 5;

 then ( angle (p2,p1,p3)) > PI by A100, Th24;

 then

 A101: ( angle (p4,p1,p3)) > PI by A88, A92, Th9;

 (p4,p1,p3) are_mutually_distinct by A27, A92, A95, ZFMISC_1:def 5;

 then ( angle (p1,p3,p4)) > PI by A101, Th24;

 then ( - ( angle (p1,p3,p4))) < ( - PI ) by XREAL_1: 24;

 then

 A102: (( - ( angle (p1,p3,p4))) + (2 * PI )) < (( - PI ) + (2 * PI )) by XREAL_1: 6;



 A103: ( cos ((2 * PI ) - ( angle (p1,p3,p4)))) = ( cos . (( - ( angle (p1,p3,p4))) + ((2 * PI ) * 1))) by SIN_COS:def 19

 .= ( cos . ( - ( angle (p1,p3,p4)))) by SIN_COS6: 10

 .= ( cos . ( angle (p1,p3,p4))) by SIN_COS: 30

 .= ( cos ( angle (p,p3,p2))) by A58, A91, SIN_COS:def 19

 .= ( cos . ( angle (p,p3,p2))) by SIN_COS:def 19

 .= ( cos . ( - ( angle (p,p3,p2)))) by SIN_COS: 30

 .= ( cos . (( - ( angle (p,p3,p2))) + ((2 * PI ) * 1))) by SIN_COS6: 10

 .= ( cos ((2 * PI ) - ( angle (p,p3,p2)))) by SIN_COS:def 19;

 ( - ( angle (p,p3,p2))) < ( - PI ) by A99, XREAL_1: 24;

 then

 A104: (( - ( angle (p,p3,p2))) + (2 * PI )) < (( - PI ) + (2 * PI )) by XREAL_1: 6;

 ( angle (p,p3,p2)) < (2 * PI ) by COMPLEX2: 70;

 then ( - ( angle (p,p3,p2))) > ( - (2 * PI )) by XREAL_1: 24;

 then

 A105: (( - ( angle (p,p3,p2))) + (2 * PI )) > (( - (2 * PI )) + (2 * PI )) by XREAL_1: 6;

 ( angle (p1,p3,p4)) < (2 * PI ) by COMPLEX2: 70;

 then ( - ( angle (p1,p3,p4))) > ( - (2 * PI )) by XREAL_1: 24;

 then (( - ( angle (p1,p3,p4))) + (2 * PI )) > (( - (2 * PI )) + (2 * PI )) by XREAL_1: 6;



 then ((2 * PI ) - ( angle (p1,p3,p4))) = ( arccos ( cos ((2 * PI ) - ( angle (p1,p3,p4))))) by A102, SIN_COS6: 92

 .= ((2 * PI ) - ( angle (p,p3,p2))) by A104, A103, A105, SIN_COS6: 92;

 hence thesis;

 end;

 end;

 end;

 theorem :: EUCLID_6:29

 p1 in ( inside_of_circle (a,b,r)) & p2 in ( outside_of_circle (a,b,r)) implies ex p st p in (( LSeg (p1,p2)) /\ ( circle (a,b,r))) by Lm17;

 theorem :: EUCLID_6:30



 Th30: p1 in ( circle (a,b,r)) & p3 in ( circle (a,b,r)) & p4 in ( circle (a,b,r)) & p in ( LSeg (p1,p3)) & p in ( LSeg (p1,p4)) & p3 <> p4 implies p = p1

 proof

 assume

 A1: p1 in ( circle (a,b,r));

 assume

 A2: p3 in ( circle (a,b,r));

 assume

 A3: p4 in ( circle (a,b,r));

 assume

 A4: p in ( LSeg (p1,p3));

 assume

 A5: p in ( LSeg (p1,p4));

 assume

 A6: p3 <> p4;

 per cases ;

 suppose

 A7: p1 = p3 or p1 = p4;

 per cases by A7;

 suppose p1 = p3;

 then p in {p1} by A4, RLTOPSP1: 70;

 hence thesis by TARSKI:def 1;

 end;

 suppose p1 = p4;

 then p in {p1} by A5, RLTOPSP1: 70;

 hence thesis by TARSKI:def 1;

 end;

 end;

 suppose

 A8: p1 <> p3 & p1 <> p4;

 per cases ;

 suppose

 A9: p <> p1;



 A10: ( inside_of_circle (a,b,r)) misses ( circle (a,b,r)) by TOPREAL9: 54;

 per cases by A4, A5, A6, A9, Th12;

 suppose

 A11: p3 in ( LSeg (p1,p4));

 not p3 in {p1, p4} by A6, A8, TARSKI:def 2;

 then

 A12: p3 in (( LSeg (p1,p4)) \ {p1, p4}) by A11, XBOOLE_0:def 5;

 (( LSeg (p1,p4)) \ {p1, p4}) c= ( inside_of_circle (a,b,r)) by A1, A3, TOPREAL9: 60;

 then p3 in (( inside_of_circle (a,b,r)) /\ ( circle (a,b,r))) by A2, A12, XBOOLE_0:def 4;

 hence thesis by A10, XBOOLE_0:def 7;

 end;

 suppose

 A13: p4 in ( LSeg (p1,p3));

 not p4 in {p1, p3} by A6, A8, TARSKI:def 2;

 then

 A14: p4 in (( LSeg (p1,p3)) \ {p1, p3}) by A13, XBOOLE_0:def 5;

 (( LSeg (p1,p3)) \ {p1, p3}) c= ( inside_of_circle (a,b,r)) by A1, A2, TOPREAL9: 60;

 then p4 in (( inside_of_circle (a,b,r)) /\ ( circle (a,b,r))) by A3, A14, XBOOLE_0:def 4;

 hence thesis by A10, XBOOLE_0:def 7;

 end;

 end;

 suppose p = p1;

 hence thesis;

 end;

 end;

 end;

 theorem :: EUCLID_6:31



 Th31: p1 in ( circle (a,b,r)) & p2 in ( circle (a,b,r)) & p in ( circle (a,b,r)) & pc = |[a, b]| & pc in ( LSeg (p,p2)) & p1 <> p implies (2 * ( angle (p1,p,p2))) = ( angle (p1,pc,p2)) or (2 * (( angle (p1,p,p2)) - PI )) = ( angle (p1,pc,p2))

 proof

 assume

 A1: p1 in ( circle (a,b,r));

 assume

 A2: p2 in ( circle (a,b,r));

 assume

 A3: p in ( circle (a,b,r));

 assume that

 A4: pc = |[a, b]| and

 A5: pc in ( LSeg (p,p2));

 assume

 A6: p1 <> p;

 per cases ;

 suppose

 A7: r = 0 ;

 then |.(p1 - pc).| = 0 by A1, A4, TOPREAL9: 43;

 then

 A8: p1 = pc by Lm1;



 A9: |.(p2 - pc).| = 0 by A2, A4, A7, TOPREAL9: 43;

 then p2 = pc by Lm1;



 then (2 * ( angle (p1,p,p2))) = (2 * 0 ) by A8, COMPLEX2: 79

 .= ( angle (pc,pc,pc)) by COMPLEX2: 79;

 hence thesis by A9, A8, Lm1;

 end;

 suppose

 A10: r <> 0 ;

 |.(p2 - pc).| = r by A2, A4, TOPREAL9: 43;

 then

 A11: pc <> p2 by A10, Lm1;



 A12: ( euc2cpx p1) <> ( euc2cpx p) by A6, EUCLID_3: 4;



 A13: |.(p1 - pc).| = r by A1, A4, TOPREAL9: 43;

 then pc <> p1 by A10, Lm1;

 then

 A14: ( euc2cpx pc) <> ( euc2cpx p1) by EUCLID_3: 4;



 A15: |.(p - pc).| = r by A3, A4, TOPREAL9: 43;

 then

 A16: pc <> p by A10, Lm1;

 then

 A17: ( angle (p1,p,p2)) = ( angle (p1,p,pc)) by A5, Th10;

 |.(pc - p1).| = |.(p - pc).| by A13, A15, Lm2;

 then

 A18: ( angle (pc,p1,p)) = ( angle (p1,p,pc)) by A6, Th16;

 ( euc2cpx pc) <> ( euc2cpx p) by A16, EUCLID_3: 4;

 then

 A19: ((( angle (pc,p1,p)) + ( angle (p1,p,pc))) + ( angle (p,pc,p1))) = PI or ((( angle (pc,p1,p)) + ( angle (p1,p,pc))) + ( angle (p,pc,p1))) = (5 * PI ) by A14, A12, COMPLEX2: 88;

 per cases by A5, A16, A11, A19, A18, A17, Th13;

 suppose (( angle (p,pc,p1)) + ( angle (p1,pc,p2))) = PI & ((2 * ( angle (p1,p,p2))) + ( angle (p,pc,p1))) = PI ;

 hence thesis;

 end;

 suppose

 A20: (( angle (p,pc,p1)) + ( angle (p1,pc,p2))) = (3 * PI ) & ((2 * ( angle (p1,p,p2))) + ( angle (p,pc,p1))) = PI ;

 ( angle (p1,pc,p2)) < (2 * PI ) & ( angle (p1,p,p2)) >= 0 by COMPLEX2: 70;

 then (( - (2 * ( angle (p1,p,p2)))) + ( angle (p1,pc,p2))) < ( 0 + (2 * PI )) by XREAL_1: 8;

 hence thesis by A20;

 end;

 suppose

 A21: (( angle (p,pc,p1)) + ( angle (p1,pc,p2))) = PI & ((2 * ( angle (p1,p,p2))) + ( angle (p,pc,p1))) = (5 * PI );

 ( angle (p1,pc,p2)) >= 0 & (( angle (p1,p,p2)) * 2) < ((2 * PI ) * 2) by COMPLEX2: 70, XREAL_1: 68;

 then ((2 * ( angle (p1,p,p2))) + ( - ( angle (p1,pc,p2)))) < (((2 * PI ) * 2) + 0 ) by XREAL_1: 8;

 hence thesis by A21;

 end;

 suppose (( angle (p,pc,p1)) + ( angle (p1,pc,p2))) = (3 * PI ) & ((2 * ( angle (p1,p,p2))) + ( angle (p,pc,p1))) = (5 * PI );

 hence thesis;

 end;

 end;

 end;

 theorem :: EUCLID_6:32



 Th32: p1 in ( circle (a,b,r)) & r > 0 implies ex p2 st p1 <> p2 & p2 in ( circle (a,b,r)) & |[a, b]| in ( LSeg (p1,p2))

 proof

 set pc = |[a, b]|;

 set p2 = ((2 * pc) - p1);

 assume

 A1: p1 in ( circle (a,b,r));

 then

 A2: |.(p1 - pc).| = r by TOPREAL9: 43;

 assume

 A3: r > 0 ;

 take p2;

 thus p1 <> p2

 proof

 assume p1 = p2;

 then ((1 * p1) + p1) = (((2 * pc) - p1) + p1) by RLVECT_1:def 8;

 then ((1 * p1) + (1 * p1)) = (((2 * pc) - p1) + p1) by RLVECT_1:def 8;

 then ((1 + 1) * p1) = (((2 * pc) - p1) + p1) by RLVECT_1:def 6;

 then (2 * p1) = ((2 * pc) - (p1 - p1)) by RLVECT_1: 29;

 then (2 * p1) = ((2 * pc) - ( 0. ( TOP-REAL 2))) by RLVECT_1: 5;

 then (2 * p1) = ((2 * pc) + ( 0. ( TOP-REAL 2))) by RLVECT_1: 12;

 then (2 * p1) = (2 * pc) by RLVECT_1: 4;

 then p1 = pc by RLVECT_1: 36;

 then |.(pc - pc).| = r by A1, TOPREAL9: 43;

 hence contradiction by A3, Lm1;

 end;

 |.(p2 - pc).| = |.(((2 * pc) - p1) - pc).|

 .= |.(((2 * pc) + ( - p1)) - pc).|

 .= |.(((2 * pc) + ( - pc)) + ( - p1)).| by RLVECT_1:def 3

 .= |.(((2 * pc) + (( - 1) * pc)) + ( - p1)).|

 .= |.(((2 + ( - 1)) * pc) + ( - p1)).| by RLVECT_1:def 6

 .= |.(pc - p1).| by RLVECT_1:def 8

 .= r by A2, Lm2;

 hence p2 in ( circle (a,b,r)) by TOPREAL9: 43;

 (((1 - (1 / 2)) * p1) + ((1 / 2) * p2)) = ((1 / 2) * (p1 + p2)) by RLVECT_1:def 5

 .= ((1 / 2) * ((p1 + ( - p1)) + (2 * pc))) by RLVECT_1:def 3

 .= ((1 / 2) * (( 0. ( TOP-REAL 2)) + (2 * pc))) by RLVECT_1: 5

 .= ((1 / 2) * (2 * pc)) by RLVECT_1: 4

 .= (((1 / 2) * 2) * pc) by RLVECT_1:def 7

 .= pc by RLVECT_1:def 8;

 hence thesis;

 end;

 theorem :: EUCLID_6:33



 Th33: p1 in ( circle (a,b,r)) & p2 in ( circle (a,b,r)) & p in ( circle (a,b,r)) & pc = |[a, b]| & p1 <> p & p2 <> p implies (2 * ( angle (p1,p,p2))) = ( angle (p1,pc,p2)) or (2 * (( angle (p1,p,p2)) - PI )) = ( angle (p1,pc,p2))

 proof

 assume

 A1: p1 in ( circle (a,b,r));

 assume

 A2: p2 in ( circle (a,b,r));

 assume

 A3: p in ( circle (a,b,r));

 assume

 A4: pc = |[a, b]|;

 assume that

 A5: p1 <> p and

 A6: p2 <> p;

 per cases ;

 suppose

 A7: r = 0 ;

 then |.(p1 - pc).| = 0 by A1, A4, TOPREAL9: 43;

 then

 A8: p1 = pc by Lm1;



 A9: |.(p2 - pc).| = 0 by A2, A4, A7, TOPREAL9: 43;

 then p2 = pc by Lm1;



 then (2 * ( angle (p1,p,p2))) = (2 * 0 ) by A8, COMPLEX2: 79

 .= ( angle (pc,pc,pc)) by COMPLEX2: 79;

 hence thesis by A9, A8, Lm1;

 end;

 suppose

 A10: r <> 0 ;



 A11: |.(p2 - pc).| = r by A2, A4, TOPREAL9: 43;

 |.(p1 - pc).| >= 0 ;

 then r > 0 by A1, A4, A10, TOPREAL9: 43;

 then

 consider p3 such that p <> p3 and

 A12: p3 in ( circle (a,b,r)) and

 A13: |[a, b]| in ( LSeg (p,p3)) by A3, Th32;

 per cases ;

 suppose p2 = p3;

 hence thesis by A1, A3, A4, A5, A12, A13, Th31;

 end;

 suppose

 A14: p2 <> p3;



 A15: ( angle (p2,pc,p3)) <> 0

 proof

 set z3 = ( euc2cpx (p3 - pc));

 set z2 = ( euc2cpx (p2 - pc));

 assume ( angle (p2,pc,p3)) = 0 ;

 then

 A16: ( Arg (p2 - pc)) = ( Arg (p3 - pc)) by EUCLID_3: 36;



 A17: |.(p2 - pc).| = |.(p3 - pc).| by A4, A11, A12, TOPREAL9: 43;



 A18: |.z2.| = |.(p2 - pc).| by EUCLID_3: 25

 .= |.z3.| by A17, EUCLID_3: 25;



 A19: z2 = (( |.z2.| * ( cos ( Arg z2))) + (( |.z2.| * ( sin ( Arg z2))) * )) by COMPTRIG: 62

 .= z3 by A16, A18, COMPTRIG: 62;

 p2 = (p2 + ( 0. ( TOP-REAL 2))) by RLVECT_1: 4

 .= (p2 + (pc + ( - pc))) by RLVECT_1: 5

 .= ((p2 + ( - pc)) + pc) by RLVECT_1:def 3

 .= ((p3 - pc) + pc) by A19, EUCLID_3: 4

 .= (p3 + (pc + ( - pc))) by RLVECT_1:def 3

 .= (p3 + ( 0. ( TOP-REAL 2))) by RLVECT_1: 5

 .= p3 by RLVECT_1: 4;

 hence contradiction by A14;

 end;

 (2 * ( angle (p2,p,p3))) = ( angle (p2,pc,p3)) or (2 * (( angle (p2,p,p3)) - PI )) = ( angle (p2,pc,p3)) by A2, A3, A4, A6, A12, A13, Th31;

 then

 A20: ( angle (p2,p,p3)) <> 0 by A15, COMPLEX2: 70;



 A21: (2 * (( angle (p2,p,p3)) - PI )) = ( angle (p2,pc,p3)) implies (2 * ( angle (p3,p,p2))) = ( angle (p3,pc,p2))

 proof

 assume

 A22: (2 * (( angle (p2,p,p3)) - PI )) = ( angle (p2,pc,p3));



 thus (2 * ( angle (p3,p,p2))) = (2 * ((2 * PI ) - ( angle (p2,p,p3)))) by A20, EUCLID_3: 37

 .= ((2 * PI ) - (2 * (( angle (p2,p,p3)) - PI )))

 .= ( angle (p3,pc,p2)) by A15, A22, EUCLID_3: 37;

 end;



 A23: ( angle (p3,p,p2)) = ((2 * PI ) - ( angle (p2,p,p3))) by A20, EUCLID_3: 37;



 A24: (2 * ( angle (p2,p,p3))) = ( angle (p2,pc,p3)) implies (2 * (( angle (p3,p,p2)) - PI )) = ( angle (p3,pc,p2))

 proof

 assume (2 * ( angle (p2,p,p3))) = ( angle (p2,pc,p3));



 hence (2 * (( angle (p3,p,p2)) - PI )) = ((2 * PI ) - ( angle (p2,pc,p3))) by A23

 .= ( angle (p3,pc,p2)) by A15, EUCLID_3: 37;

 end;



 A25: ( angle (p1,p,p2)) = (( angle (p1,p,p3)) + ( angle (p3,p,p2))) or (( angle (p1,p,p2)) + (2 * PI )) = (( angle (p1,p,p3)) + ( angle (p3,p,p2))) by Th4;

 per cases by Th4;

 suppose

 A26: ( angle (p1,pc,p2)) = (( angle (p1,pc,p3)) + ( angle (p3,pc,p2)));

 per cases by A1, A2, A3, A4, A5, A6, A12, A13, A24, A21, Th31;

 suppose (2 * ( angle (p1,p,p3))) = ( angle (p1,pc,p3)) & (2 * (( angle (p3,p,p2)) - PI )) = ( angle (p3,pc,p2));

 then ( angle (p1,pc,p2)) = ((2 * ( angle (p1,p,p2))) - (2 * PI )) or ( angle (p1,pc,p2)) = ((2 * ( angle (p1,p,p2))) + (2 * PI )) by A25, A26;

 hence thesis by Lm3;

 end;

 suppose (2 * ( angle (p1,p,p3))) = ( angle (p1,pc,p3)) & (2 * ( angle (p3,p,p2))) = ( angle (p3,pc,p2));

 then ( angle (p1,pc,p2)) = (2 * ( angle (p1,p,p2))) or ( angle (p1,pc,p2)) = ((2 * ( angle (p1,p,p2))) + (4 * PI )) by A25, A26;

 hence thesis by Lm4;

 end;

 suppose (2 * (( angle (p1,p,p3)) - PI )) = ( angle (p1,pc,p3)) & (2 * (( angle (p3,p,p2)) - PI )) = ( angle (p3,pc,p2));

 then ( angle (p1,pc,p2)) = ((2 * (( angle (p1,p,p3)) + ( angle (p3,p,p2)))) - (4 * PI )) by A26;

 hence thesis by A25, Lm5;

 end;

 suppose (2 * (( angle (p1,p,p3)) - PI )) = ( angle (p1,pc,p3)) & (2 * ( angle (p3,p,p2))) = ( angle (p3,pc,p2));

 then ( angle (p1,pc,p2)) = ((2 * ( angle (p1,p,p2))) - (2 * PI )) or ( angle (p1,pc,p2)) = ((2 * ( angle (p1,p,p2))) + (2 * PI )) by A25, A26;

 hence thesis by Lm3;

 end;

 end;

 suppose

 A27: (( angle (p1,pc,p2)) + (2 * PI )) = (( angle (p1,pc,p3)) + ( angle (p3,pc,p2)));

 per cases by A1, A2, A3, A4, A5, A6, A12, A13, A24, A21, Th31;

 suppose (2 * ( angle (p1,p,p3))) = ( angle (p1,pc,p3)) & (2 * (( angle (p3,p,p2)) - PI )) = ( angle (p3,pc,p2));

 then ( angle (p1,pc,p2)) = ((2 * (( angle (p1,p,p3)) + ( angle (p3,p,p2)))) - (4 * PI )) by A27;

 hence thesis by A25, Lm5;

 end;

 suppose (2 * ( angle (p1,p,p3))) = ( angle (p1,pc,p3)) & (2 * ( angle (p3,p,p2))) = ( angle (p3,pc,p2));

 then ( angle (p1,pc,p2)) = ((2 * ( angle (p1,p,p2))) - (2 * PI )) or ( angle (p1,pc,p2)) = ((2 * ( angle (p1,p,p2))) + (2 * PI )) by A25, A27;

 hence thesis by Lm3;

 end;

 suppose (2 * (( angle (p1,p,p3)) - PI )) = ( angle (p1,pc,p3)) & (2 * (( angle (p3,p,p2)) - PI )) = ( angle (p3,pc,p2));

 then ( angle (p1,pc,p2)) = ((2 * (( angle (p1,p,p3)) + ( angle (p3,p,p2)))) - (6 * PI )) by A27;

 hence thesis by A25, Lm6;

 end;

 suppose (2 * (( angle (p1,p,p3)) - PI )) = ( angle (p1,pc,p3)) & (2 * ( angle (p3,p,p2))) = ( angle (p3,pc,p2));

 then ( angle (p1,pc,p2)) = ((2 * (( angle (p1,p,p3)) + ( angle (p3,p,p2)))) - (4 * PI )) by A27;

 hence thesis by A25, Lm5;

 end;

 end;

 end;

 end;

 end;

 theorem :: EUCLID_6:34



 Th34: p1 in ( circle (a,b,r)) & p2 in ( circle (a,b,r)) & p3 in ( circle (a,b,r)) & p4 in ( circle (a,b,r)) & p1 <> p3 & p1 <> p4 & p2 <> p3 & p2 <> p4 implies ( angle (p1,p3,p2)) = ( angle (p1,p4,p2)) or ( angle (p1,p3,p2)) = (( angle (p1,p4,p2)) - PI ) or ( angle (p1,p3,p2)) = (( angle (p1,p4,p2)) + PI )

 proof

 assume

 A1: p1 in ( circle (a,b,r));

 set pc = |[a, b]|;

 assume

 A2: p2 in ( circle (a,b,r));

 assume

 A3: p3 in ( circle (a,b,r));

 assume

 A4: p4 in ( circle (a,b,r));

 assume that

 A5: p1 <> p3 and

 A6: p1 <> p4 and

 A7: p2 <> p3 and

 A8: p2 <> p4;

 per cases by A1, A2, A3, A5, A7, Th33;

 suppose (2 * ( angle (p1,p3,p2))) = ( angle (p1,pc,p2));

 then (2 * ( angle (p1,p4,p2))) = (2 * ( angle (p1,p3,p2))) or (2 * (( angle (p1,p4,p2)) - PI )) = (2 * ( angle (p1,p3,p2))) by A1, A2, A4, A6, A8, Th33;

 hence thesis;

 end;

 suppose (2 * (( angle (p1,p3,p2)) - PI )) = ( angle (p1,pc,p2));

 then (2 * ( angle (p1,p4,p2))) = (2 * (( angle (p1,p3,p2)) - PI )) or (2 * (( angle (p1,p4,p2)) - PI )) = (2 * (( angle (p1,p3,p2)) - PI )) by A1, A2, A4, A6, A8, Th33;

 hence thesis;

 end;

 end;

 theorem :: EUCLID_6:35



 Th35: p1 in ( circle (a,b,r)) & p2 in ( circle (a,b,r)) & p3 in ( circle (a,b,r)) & p1 <> p2 & p2 <> p3 implies ( angle (p1,p2,p3)) <> PI

 proof

 assume

 A1: p1 in ( circle (a,b,r));

 assume

 A2: p2 in ( circle (a,b,r));

 assume p3 in ( circle (a,b,r));

 then

 A3: (( LSeg (p1,p3)) \ {p1, p3}) c= ( inside_of_circle (a,b,r)) by A1, TOPREAL9: 60;

 assume p1 <> p2 & p2 <> p3;

 then

 A4: not p2 in {p1, p3} by TARSKI:def 2;

 ( inside_of_circle (a,b,r)) misses ( circle (a,b,r)) by TOPREAL9: 54;

 then

 A5: (( inside_of_circle (a,b,r)) /\ ( circle (a,b,r))) = {} by XBOOLE_0:def 7;

 assume ( angle (p1,p2,p3)) = PI ;

 then p2 in ( LSeg (p1,p3)) by Th11;

 then p2 in (( LSeg (p1,p3)) \ {p1, p3}) by A4, XBOOLE_0:def 5;

 hence contradiction by A2, A3, A5, XBOOLE_0:def 4;

 end;



 Lm22: p1 in ( circle (a,b,r)) & p3 in ( circle (a,b,r)) & p4 in ( circle (a,b,r)) & p in ( LSeg (p1,p3)) & p in ( LSeg (p1,p4)) implies ( |.(p1 - p).| * |.(p - p3).|) = ( |.(p1 - p).| * |.(p - p4).|)

 proof

 assume

 A1: p1 in ( circle (a,b,r)) & p3 in ( circle (a,b,r)) & p4 in ( circle (a,b,r));

 assume

 A2: p in ( LSeg (p1,p3)) & p in ( LSeg (p1,p4));

 per cases ;

 suppose p3 <> p4;

 then p = p1 by A1, A2, Th30;



 then |.(p1 - p).| = |.( 0. ( TOP-REAL 2)).| by RLVECT_1: 5

 .= 0 by EUCLID_2: 39;

 hence thesis;

 end;

 suppose p3 = p4;

 hence thesis;

 end;

 end;



 Lm23: p1 in ( circle (a,b,r)) & p2 in ( circle (a,b,r)) & p4 in ( circle (a,b,r)) & p in ( LSeg (p1,p1)) & p in ( LSeg (p2,p4)) implies ( |.(p1 - p).| * |.(p - p1).|) = ( |.(p2 - p).| * |.(p - p4).|)

 proof

 assume that

 A1: p1 in ( circle (a,b,r)) and

 A2: p2 in ( circle (a,b,r)) & p4 in ( circle (a,b,r));



 A3: (( LSeg (p2,p4)) \ {p2, p4}) c= ( inside_of_circle (a,b,r)) by A2, TOPREAL9: 60;



 A4: ( inside_of_circle (a,b,r)) misses ( circle (a,b,r)) by TOPREAL9: 54;

 assume p in ( LSeg (p1,p1));

 then

 A5: p in {p1} by RLTOPSP1: 70;



 then

 A6: |.(p1 - p).| = |.(p - p).| by TARSKI:def 1

 .= |.( 0. ( TOP-REAL 2)).| by RLVECT_1: 5

 .= |.( 0* 2).| by EUCLID: 70

 .= 0 by EUCLID: 7;

 assume p in ( LSeg (p2,p4));

 then

 A7: p1 in ( LSeg (p2,p4)) by A5, TARSKI:def 1;

 per cases ;

 suppose p1 <> p2 & p1 <> p4;

 then not p1 in {p2, p4} by TARSKI:def 2;

 then p1 in (( LSeg (p2,p4)) \ {p2, p4}) by A7, XBOOLE_0:def 5;

 then p1 in (( inside_of_circle (a,b,r)) /\ ( circle (a,b,r))) by A1, A3, XBOOLE_0:def 4;

 hence thesis by A4, XBOOLE_0:def 7;

 end;

 suppose

 A8: not (p1 <> p2 & p1 <> p4);

 per cases by A8;

 suppose p1 = p2;



 then |.(p2 - p).| = |.(p1 - p1).| by A5, TARSKI:def 1

 .= |.( 0. ( TOP-REAL 2)).| by RLVECT_1: 5

 .= |.( 0* 2).| by EUCLID: 70

 .= 0 by EUCLID: 7;

 hence thesis by A6;

 end;

 suppose p1 = p4;



 then |.(p - p4).| = |.(p1 - p1).| by A5, TARSKI:def 1

 .= |.( 0. ( TOP-REAL 2)).| by RLVECT_1: 5

 .= |.( 0* 2).| by EUCLID: 70

 .= 0 by EUCLID: 7;

 hence thesis by A6;

 end;

 end;

 end;

 theorem :: EUCLID_6:36



 Th36: p1 in ( circle (a,b,r)) & p2 in ( circle (a,b,r)) & p3 in ( circle (a,b,r)) & p4 in ( circle (a,b,r)) & p in ( LSeg (p1,p3)) & p in ( LSeg (p2,p4)) & (p1,p2,p3,p4) are_mutually_distinct implies ( angle (p1,p4,p2)) = ( angle (p1,p3,p2))

 proof

 assume that

 A1: p1 in ( circle (a,b,r)) and

 A2: p2 in ( circle (a,b,r)) and

 A3: p3 in ( circle (a,b,r)) and

 A4: p4 in ( circle (a,b,r));



 A5: (( LSeg (p1,p3)) \ {p1, p3}) c= ( inside_of_circle (a,b,r)) by A1, A3, TOPREAL9: 60;

 assume that

 A6: p in ( LSeg (p1,p3)) and

 A7: p in ( LSeg (p2,p4));

 assume

 A8: (p1,p2,p3,p4) are_mutually_distinct ;

 then

 A9: p1 <> p2 by ZFMISC_1:def 6;



 A10: p3 <> p4 by A8, ZFMISC_1:def 6;



 A11: p1 <> p4 by A8, ZFMISC_1:def 6;



 A12: p2 <> p4 by A8, ZFMISC_1:def 6;



 A13: p1 <> p3 by A8, ZFMISC_1:def 6;



 A14: ( inside_of_circle (a,b,r)) misses ( circle (a,b,r)) by TOPREAL9: 54;



 A15: (( LSeg (p2,p4)) \ {p2, p4}) c= ( inside_of_circle (a,b,r)) by A2, A4, TOPREAL9: 60;



 A16: p <> p1 & p <> p4

 proof

 assume

 A17: p = p1 or p = p4;

 per cases by A17;

 suppose

 A18: p = p1;

 not p1 in {p2, p4} by A9, A11, TARSKI:def 2;

 then p1 in (( LSeg (p2,p4)) \ {p2, p4}) by A7, A18, XBOOLE_0:def 5;

 then p1 in (( inside_of_circle (a,b,r)) /\ ( circle (a,b,r))) by A1, A15, XBOOLE_0:def 4;

 hence contradiction by A14, XBOOLE_0:def 7;

 end;

 suppose

 A19: p = p4;

 not p4 in {p1, p3} by A11, A10, TARSKI:def 2;

 then p4 in (( LSeg (p1,p3)) \ {p1, p3}) by A6, A19, XBOOLE_0:def 5;

 then p4 in (( inside_of_circle (a,b,r)) /\ ( circle (a,b,r))) by A4, A5, XBOOLE_0:def 4;

 hence contradiction by A14, XBOOLE_0:def 7;

 end;

 end;

 then

 A20: (p1,p4,p) are_mutually_distinct by A11, ZFMISC_1:def 5;



 A21: (p4,p,p1) are_mutually_distinct by A11, A16, ZFMISC_1:def 5;



 A22: ( angle (p1,p4,p)) = ( angle (p1,p4,p2)) by A7, A16, Th10;



 A23: p2 <> p3 by A8, ZFMISC_1:def 6;



 A24: p <> p2 & p <> p3

 proof

 assume

 A25: p = p2 or p = p3;

 per cases by A25;

 suppose

 A26: p = p3;

 not p3 in {p2, p4} by A23, A10, TARSKI:def 2;

 then p3 in (( LSeg (p2,p4)) \ {p2, p4}) by A7, A26, XBOOLE_0:def 5;

 then p3 in (( inside_of_circle (a,b,r)) /\ ( circle (a,b,r))) by A3, A15, XBOOLE_0:def 4;

 hence contradiction by A14, XBOOLE_0:def 7;

 end;

 suppose

 A27: p = p2;

 not p2 in {p1, p3} by A9, A23, TARSKI:def 2;

 then p2 in (( LSeg (p1,p3)) \ {p1, p3}) by A6, A27, XBOOLE_0:def 5;

 then p2 in (( inside_of_circle (a,b,r)) /\ ( circle (a,b,r))) by A2, A5, XBOOLE_0:def 4;

 hence contradiction by A14, XBOOLE_0:def 7;

 end;

 end;

 then

 A28: ( angle (p4,p,p1)) = ( angle (p2,p,p3)) by A6, A7, A16, Th15;



 A29: (p,p3,p2) are_mutually_distinct by A23, A24, ZFMISC_1:def 5;



 A30: (p2,p,p3) are_mutually_distinct by A23, A24, ZFMISC_1:def 5;



 A31: ( angle (p,p3,p2)) = ( angle (p1,p3,p2)) by A6, A24, Th9;

 per cases by A1, A2, A3, A4, A13, A11, A23, A12, Th34;

 suppose ( angle (p1,p4,p2)) = ( angle (p1,p3,p2));

 hence thesis;

 end;

 suppose

 A32: ( angle (p1,p4,p2)) = (( angle (p1,p3,p2)) - PI );

 ( angle (p1,p3,p2)) < (2 * PI ) by COMPLEX2: 70;

 then (( angle (p1,p3,p2)) - PI ) < ((2 * PI ) - PI ) by XREAL_1: 9;

 then ( angle (p2,p,p3)) <= PI by A22, A28, A20, A32, Th23;

 then

 A33: ( angle (p1,p3,p2)) <= PI by A31, A30, Th23;



 A34: not p3 in {p1, p2} by A13, A23, TARSKI:def 2;

 ( angle (p1,p4,p2)) >= 0 by COMPLEX2: 70;

 then ((( angle (p1,p3,p2)) - PI ) + PI ) >= ( 0 + PI ) by A32, XREAL_1: 6;

 then p3 in ( LSeg (p1,p2)) by A33, Th11, XXREAL_0: 1;

 then

 A35: p3 in (( LSeg (p1,p2)) \ {p1, p2}) by A34, XBOOLE_0:def 5;

 (( LSeg (p1,p2)) \ {p1, p2}) c= ( inside_of_circle (a,b,r)) by A1, A2, TOPREAL9: 60;

 then ( inside_of_circle (a,b,r)) misses ( circle (a,b,r)) & p3 in (( inside_of_circle (a,b,r)) /\ ( circle (a,b,r))) by A3, A35, TOPREAL9: 54, XBOOLE_0:def 4;

 hence thesis by XBOOLE_0:def 7;

 end;

 suppose

 A36: ( angle (p1,p4,p2)) = (( angle (p1,p3,p2)) + PI );

 ( angle (p1,p4,p2)) < (2 * PI ) by COMPLEX2: 70;

 then (( angle (p1,p4,p2)) - PI ) < ((2 * PI ) - PI ) by XREAL_1: 9;

 then ( angle (p4,p,p1)) <= PI by A31, A28, A29, A36, Th23;

 then

 A37: ( angle (p1,p4,p2)) <= PI by A22, A21, Th23;



 A38: not p4 in {p1, p2} by A11, A12, TARSKI:def 2;

 ( angle (p1,p3,p2)) >= 0 by COMPLEX2: 70;

 then ((( angle (p1,p4,p2)) - PI ) + PI ) >= ( 0 + PI ) by A36, XREAL_1: 6;

 then p4 in ( LSeg (p1,p2)) by A37, Th11, XXREAL_0: 1;

 then

 A39: p4 in (( LSeg (p1,p2)) \ {p1, p2}) by A38, XBOOLE_0:def 5;

 (( LSeg (p1,p2)) \ {p1, p2}) c= ( inside_of_circle (a,b,r)) by A1, A2, TOPREAL9: 60;

 then ( inside_of_circle (a,b,r)) misses ( circle (a,b,r)) & p4 in (( inside_of_circle (a,b,r)) /\ ( circle (a,b,r))) by A4, A39, TOPREAL9: 54, XBOOLE_0:def 4;

 hence thesis by XBOOLE_0:def 7;

 end;

 end;

 theorem :: EUCLID_6:37



 Th37: p1 in ( circle (a,b,r)) & p2 in ( circle (a,b,r)) & p3 in ( circle (a,b,r)) & ( angle (p1,p2,p3)) = 0 & p1 <> p2 & p2 <> p3 implies p1 = p3

 proof

 assume

 A1: p1 in ( circle (a,b,r)) & p2 in ( circle (a,b,r)) & p3 in ( circle (a,b,r));

 assume

 A2: ( angle (p1,p2,p3)) = 0 ;

 assume

 A3: p1 <> p2 & p2 <> p3;

 then

 A4: ( euc2cpx p1) <> ( euc2cpx p2) & ( euc2cpx p2) <> ( euc2cpx p3) by EUCLID_3: 4;

 assume

 A5: p1 <> p3;

 then ( euc2cpx p1) <> ( euc2cpx p3) by EUCLID_3: 4;

 then ( angle (p2,p3,p1)) = 0 & ( angle (p3,p1,p2)) = PI or ( angle (p2,p3,p1)) = PI & ( angle (p3,p1,p2)) = 0 by A2, A4, COMPLEX2: 87;

 hence contradiction by A1, A3, A5, Th35;

 end;

 ::$Notion-Name

 theorem :: EUCLID_6:38

 p1 in ( circle (a,b,r)) & p2 in ( circle (a,b,r)) & p3 in ( circle (a,b,r)) & p4 in ( circle (a,b,r)) & p in ( LSeg (p1,p3)) & p in ( LSeg (p2,p4)) implies ( |.(p1 - p).| * |.(p - p3).|) = ( |.(p2 - p).| * |.(p - p4).|)

 proof

 assume that

 A1: p1 in ( circle (a,b,r)) and

 A2: p2 in ( circle (a,b,r)) and

 A3: p3 in ( circle (a,b,r)) and

 A4: p4 in ( circle (a,b,r));



 A5: |.(p1 - p).| = |.(p - p1).| by Lm2;



 A6: |.(p3 - p).| = |.(p - p3).| by Lm2;



 A7: |.(p2 - p).| = |.(p - p2).| & |.(p4 - p).| = |.(p - p4).| by Lm2;

 assume that

 A8: p in ( LSeg (p1,p3)) and

 A9: p in ( LSeg (p2,p4));

 per cases ;

 suppose

 A10: not (p1,p2,p3,p4) are_mutually_distinct ;

 per cases by A10, ZFMISC_1:def 6;

 suppose p1 = p2;

 hence thesis by A1, A3, A4, A8, A9, Lm22;

 end;

 suppose p1 = p3;

 hence thesis by A1, A2, A4, A8, A9, Lm23;

 end;

 suppose p1 = p4;

 hence thesis by A1, A2, A3, A8, A9, A7, Lm22;

 end;

 suppose p2 = p3;

 hence thesis by A1, A2, A4, A8, A9, A5, A6, Lm22;

 end;

 suppose p2 = p4;

 hence thesis by A1, A2, A3, A8, A9, Lm23;

 end;

 suppose p3 = p4;

 hence thesis by A1, A2, A3, A8, A9, A5, A7, Lm22;

 end;

 end;

 suppose

 A11: (p1,p2,p3,p4) are_mutually_distinct ;

 then

 A12: p3 <> p4 by ZFMISC_1:def 6;



 A13: p1 <> p2 by A11, ZFMISC_1:def 6;



 A14: p2 <> p3 by A11, ZFMISC_1:def 6;



 A15: (( LSeg (p1,p3)) \ {p1, p3}) c= ( inside_of_circle (a,b,r)) by A1, A3, TOPREAL9: 60;



 A16: ( inside_of_circle (a,b,r)) misses ( circle (a,b,r)) by TOPREAL9: 54;



 A17: (( LSeg (p2,p4)) \ {p2, p4}) c= ( inside_of_circle (a,b,r)) by A2, A4, TOPREAL9: 60;



 A18: p <> p2 & p <> p3

 proof

 assume

 A19: p = p2 or p = p3;

 per cases by A19;

 suppose

 A20: p = p3;

 not p3 in {p2, p4} by A14, A12, TARSKI:def 2;

 then p3 in (( LSeg (p2,p4)) \ {p2, p4}) by A9, A20, XBOOLE_0:def 5;

 then p3 in (( inside_of_circle (a,b,r)) /\ ( circle (a,b,r))) by A3, A17, XBOOLE_0:def 4;

 hence contradiction by A16, XBOOLE_0:def 7;

 end;

 suppose

 A21: p = p2;

 not p2 in {p1, p3} by A13, A14, TARSKI:def 2;

 then p2 in (( LSeg (p1,p3)) \ {p1, p3}) by A8, A21, XBOOLE_0:def 5;

 then p2 in (( inside_of_circle (a,b,r)) /\ ( circle (a,b,r))) by A2, A15, XBOOLE_0:def 4;

 hence contradiction by A16, XBOOLE_0:def 7;

 end;

 end;

 then

 A22: (p2,p,p3) are_mutually_distinct by A14, ZFMISC_1:def 5;



 A23: p1 <> p4 by A11, ZFMISC_1:def 6;



 A24: p <> p1 & p <> p4

 proof

 assume

 A25: p = p1 or p = p4;

 per cases by A25;

 suppose

 A26: p = p1;

 not p1 in {p2, p4} by A13, A23, TARSKI:def 2;

 then p1 in (( LSeg (p2,p4)) \ {p2, p4}) by A9, A26, XBOOLE_0:def 5;

 then p1 in (( inside_of_circle (a,b,r)) /\ ( circle (a,b,r))) by A1, A17, XBOOLE_0:def 4;

 hence contradiction by A16, XBOOLE_0:def 7;

 end;

 suppose

 A27: p = p4;

 not p4 in {p1, p3} by A23, A12, TARSKI:def 2;

 then p4 in (( LSeg (p1,p3)) \ {p1, p3}) by A8, A27, XBOOLE_0:def 5;

 then p4 in (( inside_of_circle (a,b,r)) /\ ( circle (a,b,r))) by A4, A15, XBOOLE_0:def 4;

 hence contradiction by A16, XBOOLE_0:def 7;

 end;

 end;

 then

 A28: ( angle (p4,p,p1)) = ( angle (p2,p,p3)) by A8, A9, A18, Th15;



 A29: p2 <> p4 by A11, ZFMISC_1:def 6;



 A30: ( angle (p3,p2,p)) <> PI

 proof

 assume ( angle (p3,p2,p)) = PI ;

 then ( angle (p3,p2,p4)) = PI by A9, A18, Th10;

 hence contradiction by A2, A3, A4, A14, A29, Th35;

 end;



 A31: p1 <> p3 by A11, ZFMISC_1:def 6;



 A32: ( angle (p,p3,p2)) <> PI

 proof

 assume ( angle (p,p3,p2)) = PI ;

 then ( angle (p1,p3,p2)) = PI by A8, A18, Th9;

 hence contradiction by A1, A2, A3, A31, A14, Th35;

 end;



 A33: ( angle (p,p1,p4)) <> PI

 proof

 assume ( angle (p,p1,p4)) = PI ;

 then ( angle (p3,p1,p4)) = PI by A8, A24, Th9;

 hence contradiction by A1, A3, A4, A31, A23, Th35;

 end;



 A34: ( angle (p,p3,p2)) = ( angle (p1,p3,p2)) by A8, A18, Th9;



 A35: ( angle (p1,p4,p)) = ( angle (p1,p4,p2)) by A9, A24, Th10;



 A36: ( angle (p4,p,p1)) <> PI

 proof

 assume ( angle (p4,p,p1)) = PI ;

 then p in ( LSeg (p1,p4)) by Th11;

 hence contradiction by A1, A2, A4, A9, A13, A24, Th30;

 end;

 then ( angle (p2,p,p3)) <> PI by A8, A9, A24, A18, Th15;

 then

 A37: (p2,p,p3) is_a_triangle by A22, A32, A30, Th20;



 A38: ( angle (p1,p4,p)) <> PI

 proof

 assume ( angle (p1,p4,p)) = PI ;

 then ( angle (p1,p4,p2)) = PI by A9, A24, Th10;

 hence contradiction by A1, A2, A4, A23, A29, Th35;

 end;

 (p4,p,p1) are_mutually_distinct by A23, A24, ZFMISC_1:def 5;

 then

 A39: (p4,p,p1) is_a_triangle by A36, A33, A38, Th20;

 ( angle (p1,p4,p2)) = ( angle (p1,p3,p2)) by A1, A2, A3, A4, A8, A9, A11, Th36;

 hence thesis by A5, A6, A7, A35, A34, A28, A39, A37, Th22;

 end;

 end;

 begin

 ::$Notion-Name

 theorem :: EUCLID_6:39

 a = |.(p2 - p1).| & b = |.(p3 - p2).| & c = |.(p1 - p3).| & s = (( the_perimeter_of_polygon3 (p1,p2,p3)) / 2) implies |.( the_area_of_polygon3 (p1,p2,p3)).| = ( sqrt (((s * (s - a)) * (s - b)) * (s - c)))

 proof

 assume that

 A1: a = |.(p2 - p1).| and

 A2: b = |.(p3 - p2).| and

 A3: c = |.(p1 - p3).|;



 A4: a = |.(p1 - p2).| by A1, Lm2;

 c = |.(p3 - p1).| by A3, Lm2;

 then

 A5: (c ^2 ) = (((a ^2 ) + (b ^2 )) - (((2 * a) * b) * ( cos ( angle (p1,p2,p3))))) by A2, A4, Th7;

 assume

 A6: s = (( the_perimeter_of_polygon3 (p1,p2,p3)) / 2);



 A7: ((( sin ( angle (p3,p2,p1))) ^2 ) + (( cos ( angle (p3,p2,p1))) ^2 )) = 1 by SIN_COS: 29;

 (( the_area_of_polygon3 (p1,p2,p3)) ^2 ) = ((((a * b) * ( sin ( angle (p3,p2,p1)))) / 2) ^2 ) by A2, A4, Th5

 .= ((((a * b) * ( sin ( angle (p3,p2,p1)))) ^2 ) * ((1 / 2) ^2 ))

 .= ((((a * b) ^2 ) * (1 - (( cos ( angle (p3,p2,p1))) ^2 ))) * ((1 / 2) ^2 )) by A7, SQUARE_1: 9

 .= ((((((a * b) ^2 ) - (((a * b) ^2 ) * (( cos ( angle (p3,p2,p1))) ^2 ))) * (2 ^2 )) / (2 ^2 )) * ((1 / 2) ^2 )) by XCMPLX_1: 89

 .= (((((2 ^2 ) * ((a * b) ^2 )) - ((((2 * a) * b) * ( cos ( angle (p3,p2,p1)))) ^2 )) / (2 ^2 )) * ((1 / 2) ^2 ))

 .= (((((2 ^2 ) * ((a * b) ^2 )) - (((( - (c ^2 )) + (a ^2 )) + (b ^2 )) ^2 )) / (2 ^2 )) * ((1 / 2) ^2 )) by A5, Th3

 .= (((((16 * (s - a)) * (s - b)) * ((s - c) * s)) / (2 * 2)) * ((1 / 2) ^2 )) by A1, A2, A3, A6

 .= (((s * (s - a)) * (s - b)) * (s - c));

 hence thesis by COMPLEX1: 72;

 end;

 ::$Notion-Name

 theorem :: EUCLID_6:40

 p1 in ( circle (a,b,r)) & p2 in ( circle (a,b,r)) & p3 in ( circle (a,b,r)) & p4 in ( circle (a,b,r)) & p in ( LSeg (p1,p3)) & p in ( LSeg (p2,p4)) implies ( |.(p3 - p1).| * |.(p4 - p2).|) = (( |.(p2 - p1).| * |.(p4 - p3).|) + ( |.(p3 - p2).| * |.(p4 - p1).|))

 proof

 assume that

 A1: p1 in ( circle (a,b,r)) and

 A2: p2 in ( circle (a,b,r)) and

 A3: p3 in ( circle (a,b,r)) and

 A4: p4 in ( circle (a,b,r));



 A5: |.(p3 - p1).| = |.(p1 - p3).| by Lm2;

 assume that

 A6: p in ( LSeg (p1,p3)) and

 A7: p in ( LSeg (p2,p4));

 per cases ;

 suppose

 A8: not (p1,p2,p3,p4) are_mutually_distinct ;

 per cases by A8, ZFMISC_1:def 6;

 suppose

 A9: p1 = p2;

 then |.(p2 - p1).| = 0 by Lm1;

 hence thesis by A9;

 end;

 suppose p1 = p3;

 then

 A10: p in {p1} by A6, RLTOPSP1: 70;

 then p in ( circle (a,b,r)) by A1, TARSKI:def 1;

 then p in (( LSeg (p2,p4)) /\ ( circle (a,b,r))) by A7, XBOOLE_0:def 4;

 then p in {p2, p4} by A2, A4, TOPREAL9: 61;

 then

 A11: p = p2 or p = p4 by TARSKI:def 2;

 per cases by A10, A11, TARSKI:def 1;

 suppose

 A12: p1 = p2;

 then |.(p2 - p1).| = 0 by Lm1;

 hence thesis by A12;

 end;

 suppose

 A13: p1 = p4;

 then |.(p4 - p1).| = 0 by Lm1;

 hence thesis by A5, A13, Lm2;

 end;

 end;

 suppose

 A14: p1 = p4;

 then |.(p4 - p1).| = 0 by Lm1;

 hence thesis by A5, A14, Lm2;

 end;

 suppose

 A15: p2 = p3;

 then |.(p3 - p2).| = 0 by Lm1;

 hence thesis by A15;

 end;

 suppose p2 = p4;

 then

 A16: p in {p2} by A7, RLTOPSP1: 70;

 then p in ( circle (a,b,r)) by A2, TARSKI:def 1;

 then p in (( LSeg (p1,p3)) /\ ( circle (a,b,r))) by A6, XBOOLE_0:def 4;

 then p in {p1, p3} by A1, A3, TOPREAL9: 61;

 then

 A17: p = p1 or p = p3 by TARSKI:def 2;

 per cases by A16, A17, TARSKI:def 1;

 suppose

 A18: p1 = p2;

 then |.(p2 - p1).| = 0 by Lm1;

 hence thesis by A18;

 end;

 suppose

 A19: p2 = p3;

 then |.(p3 - p2).| = 0 by Lm1;

 hence thesis by A19;

 end;

 end;

 suppose

 A20: p3 = p4;

 then |.(p4 - p3).| = 0 by Lm1;

 hence thesis by A20;

 end;

 end;

 suppose

 A21: (p1,p2,p3,p4) are_mutually_distinct ;

 then

 A22: p3 <> p4 by ZFMISC_1:def 6;

 then

 A23: ( euc2cpx p3) <> ( euc2cpx p4) by EUCLID_3: 4;



 A24: p2 <> p4 by A21, ZFMISC_1:def 6;

 then

 A25: ( angle (p3,p4,p2)) <> PI by A2, A3, A4, A22, Th35;



 A26: p1 <> p2 by A21, ZFMISC_1:def 6;

 then

 A27: ( angle (p1,p2,p4)) <> PI by A1, A2, A4, A24, Th35;



 A28: p1 <> p4 by A21, ZFMISC_1:def 6;

 then

 A29: ( angle (p4,p1,p2)) <> PI by A1, A2, A4, A26, Th35;



 A30: ( angle (p2,p4,p1)) <> PI by A1, A2, A4, A28, A24, Th35;

 (p2,p4,p1) are_mutually_distinct by A26, A28, A24, ZFMISC_1:def 5;

 then

 A31: (p2,p4,p1) is_a_triangle by A30, A29, A27, Th20;



 A32: p2 <> p3 by A21, ZFMISC_1:def 6;

 then

 A33: ( euc2cpx p2) <> ( euc2cpx p3) by EUCLID_3: 4;



 A34: ( angle (p2,p3,p4)) <> PI by A2, A3, A4, A32, A22, Th35;



 A35: not p2 in ( LSeg (p1,p3))

 proof

 assume

 A36: p2 in ( LSeg (p1,p3));

 not p2 in {p1, p3} by A26, A32, TARSKI:def 2;

 then

 A37: p2 in (( LSeg (p1,p3)) \ {p1, p3}) by A36, XBOOLE_0:def 5;

 (( LSeg (p1,p3)) \ {p1, p3}) c= ( inside_of_circle (a,b,r)) by A1, A3, TOPREAL9: 60;

 then ( inside_of_circle (a,b,r)) misses ( circle (a,b,r)) & p2 in (( inside_of_circle (a,b,r)) /\ ( circle (a,b,r))) by A2, A37, TOPREAL9: 54, XBOOLE_0:def 4;

 hence contradiction by XBOOLE_0:def 7;

 end;

 then

 consider p5 such that

 A38: p5 in ( LSeg (p1,p3)) and

 A39: ( angle (p1,p2,p5)) = ( angle (p,p2,p3)) by A6, Th28;



 A40: ( angle (p4,p2,p3)) <> PI by A2, A3, A4, A32, A24, Th35;

 then

 A41: ( angle (p1,p2,p5)) <> PI by A6, A7, A35, A39, Th9;



 A42: ( euc2cpx p2) <> ( euc2cpx p4) by A24, EUCLID_3: 4;



 A43: p5 <> p1

 proof

 assume p5 = p1;



 then ( angle (p4,p2,p3)) = ( angle (p1,p2,p1)) by A6, A7, A35, A39, Th9

 .= 0 by COMPLEX2: 79;

 hence contradiction by A34, A25, A33, A42, A23, COMPLEX2: 87;

 end;



 A44: p5 <> p3

 proof

 (( angle (p4,p2,p3)) + ( angle (p3,p2,p4))) = ( angle (p4,p2,p4)) or (( angle (p4,p2,p3)) + ( angle (p3,p2,p4))) = (( angle (p4,p2,p4)) + (2 * PI )) by Th4;

 then

 A45: (( angle (p4,p2,p3)) + ( angle (p3,p2,p4))) = 0 or (( angle (p4,p2,p3)) + ( angle (p3,p2,p4))) = ( 0 + (2 * PI )) by COMPLEX2: 79;

 assume p5 = p3;

 then

 A46: ( angle (p4,p2,p3)) = ( angle (p1,p2,p3)) by A6, A7, A35, A39, Th9;

 per cases by A45, Th4;

 suppose (( angle (p4,p2,p3)) + ( angle (p3,p2,p4))) = 0 & (( angle (p1,p2,p3)) + ( angle (p3,p2,p4))) = ( angle (p1,p2,p4)) or (( angle (p4,p2,p3)) + ( angle (p3,p2,p4))) = (2 * PI ) & (( angle (p1,p2,p3)) + ( angle (p3,p2,p4))) = (( angle (p1,p2,p4)) + (2 * PI ));

 hence contradiction by A1, A2, A4, A26, A28, A24, A46, Th37;

 end;

 suppose (( angle (p4,p2,p3)) + ( angle (p3,p2,p4))) = (2 * PI ) & (( angle (p1,p2,p3)) + ( angle (p3,p2,p4))) = ( angle (p1,p2,p4));

 hence contradiction by A46, COMPLEX2: 70;

 end;

 suppose (( angle (p4,p2,p3)) + ( angle (p3,p2,p4))) = 0 & (( angle (p1,p2,p3)) + ( angle (p3,p2,p4))) = (( angle (p1,p2,p4)) + (2 * PI ));

 then ( angle (p1,p2,p4)) = ( - (2 * PI )) by A46;

 hence contradiction by COMPLEX2: 70;

 end;

 end;



 A47: ( angle (p,p2,p3)) = ( angle (p4,p2,p3)) by A6, A7, A35, Th9;



 A48: ( angle (p5,p2,p3)) = ( angle (p1,p2,p4))

 proof

 per cases by A47, A39, Th4;

 suppose ( angle (p5,p2,p3)) = (( angle (p5,p2,p4)) + ( angle (p4,p2,p3))) & ( angle (p1,p2,p4)) = (( angle (p4,p2,p3)) + ( angle (p5,p2,p4))) or (( angle (p5,p2,p3)) + (2 * PI )) = (( angle (p5,p2,p4)) + ( angle (p4,p2,p3))) & (( angle (p1,p2,p4)) + (2 * PI )) = (( angle (p4,p2,p3)) + ( angle (p5,p2,p4)));

 hence thesis;

 end;

 suppose

 A49: (( angle (p5,p2,p3)) + (2 * PI )) = (( angle (p5,p2,p4)) + ( angle (p4,p2,p3))) & ( angle (p1,p2,p4)) = (( angle (p4,p2,p3)) + ( angle (p5,p2,p4)));

 ( angle (p5,p2,p3)) >= 0 by COMPLEX2: 70;

 then (( angle (p5,p2,p3)) + (2 * PI )) >= ( 0 + (2 * PI )) by XREAL_1: 6;

 hence thesis by A49, COMPLEX2: 70;

 end;

 suppose

 A50: ( angle (p5,p2,p3)) = (( angle (p5,p2,p4)) + ( angle (p4,p2,p3))) & (( angle (p1,p2,p4)) + (2 * PI )) = (( angle (p4,p2,p3)) + ( angle (p5,p2,p4)));

 ( angle (p1,p2,p4)) >= 0 by COMPLEX2: 70;

 then (( angle (p1,p2,p4)) + (2 * PI )) >= ( 0 + (2 * PI )) by XREAL_1: 6;

 hence thesis by A50, COMPLEX2: 70;

 end;

 end;



 A51: p5 <> p2

 proof



 A52: (( LSeg (p1,p3)) \ {p1, p3}) c= ( inside_of_circle (a,b,r)) by A1, A3, TOPREAL9: 60;

 assume

 A53: p5 = p2;

 not p2 in {p1, p3} by A26, A32, TARSKI:def 2;

 then p2 in (( LSeg (p1,p3)) \ {p1, p3}) by A38, A53, XBOOLE_0:def 5;

 then ( inside_of_circle (a,b,r)) misses ( circle (a,b,r)) & p2 in (( inside_of_circle (a,b,r)) /\ ( circle (a,b,r))) by A2, A52, TOPREAL9: 54, XBOOLE_0:def 4;

 hence contradiction by XBOOLE_0:def 7;

 end;

 then

 A54: (p1,p2,p5) are_mutually_distinct by A26, A43, ZFMISC_1:def 5;

 p1 <> p3 by A21, ZFMISC_1:def 6;

 then (p2,p3,p4,p1) are_mutually_distinct by A26, A28, A32, A24, A22, ZFMISC_1:def 6;

 then

 A55: ( angle (p2,p1,p3)) = ( angle (p2,p4,p3)) by A1, A2, A3, A4, A6, A7, Th36;



 A56: ( angle (p3,p1,p2)) = ( angle (p3,p4,p2))

 proof

 per cases ;

 suppose

 A57: ( angle (p2,p1,p3)) = 0 ;

 then ( angle (p3,p1,p2)) = 0 by EUCLID_3: 36;

 hence thesis by A55, A57, EUCLID_3: 36;

 end;

 suppose

 A58: ( angle (p2,p1,p3)) <> 0 ;

 then ( angle (p3,p1,p2)) = ((2 * PI ) - ( angle (p2,p1,p3))) by EUCLID_3: 37;

 hence thesis by A55, A58, EUCLID_3: 37;

 end;

 end;

 then

 A59: ( angle (p5,p1,p2)) = ( angle (p3,p4,p2)) by A38, A43, Th9;



 A60: ( angle (p2,p3,p4)) = ( angle (p2,p5,p1))

 proof



 A61: ( euc2cpx p2) <> ( euc2cpx p5) & ( euc2cpx p2) <> ( euc2cpx p1) by A26, A51, EUCLID_3: 4;



 A62: ( euc2cpx p5) <> ( euc2cpx p1) by A43, EUCLID_3: 4;

 per cases by A33, A42, A23, A61, A62, COMPLEX2: 88;

 suppose ((( angle (p2,p3,p4)) + ( angle (p3,p4,p2))) + ( angle (p4,p2,p3))) = PI & ((( angle (p2,p5,p1)) + ( angle (p5,p1,p2))) + ( angle (p1,p2,p5))) = PI or ((( angle (p2,p3,p4)) + ( angle (p3,p4,p2))) + ( angle (p4,p2,p3))) = (5 * PI ) & ((( angle (p2,p5,p1)) + ( angle (p5,p1,p2))) + ( angle (p1,p2,p5))) = (5 * PI );

 hence thesis by A47, A39, A59;

 end;

 suppose

 A63: ((( angle (p2,p3,p4)) + ( angle (p3,p4,p2))) + ( angle (p4,p2,p3))) = (5 * PI ) & ((( angle (p2,p5,p1)) + ( angle (p5,p1,p2))) + ( angle (p1,p2,p5))) = PI ;

 ( angle (p2,p3,p4)) < (2 * PI ) & ( angle (p2,p5,p1)) >= 0 by COMPLEX2: 70;

 then

 A64: (( angle (p2,p3,p4)) - ( angle (p2,p5,p1))) < ((2 * PI ) - 0 ) by XREAL_1: 14;

 (( angle (p2,p3,p4)) - ( angle (p2,p5,p1))) = (4 * PI ) by A47, A39, A59, A63;

 hence thesis by A64, XREAL_1: 64;

 end;

 suppose

 A65: ((( angle (p2,p3,p4)) + ( angle (p3,p4,p2))) + ( angle (p4,p2,p3))) = PI & ((( angle (p2,p5,p1)) + ( angle (p5,p1,p2))) + ( angle (p1,p2,p5))) = (5 * PI );

 ( angle (p2,p5,p1)) < (2 * PI ) & ( angle (p2,p3,p4)) >= 0 by COMPLEX2: 70;

 then

 A66: (( angle (p2,p5,p1)) - ( angle (p2,p3,p4))) < ((2 * PI ) - 0 ) by XREAL_1: 14;

 (( angle (p2,p5,p1)) - ( angle (p2,p3,p4))) = (4 * PI ) by A47, A39, A59, A65;

 hence thesis by A66, XREAL_1: 64;

 end;

 end;



 A67: ( angle (p1,p4,p2)) = ( angle (p1,p3,p2)) by A1, A2, A3, A4, A6, A7, A21, Th36;

 ( angle (p2,p4,p1)) = ( angle (p2,p3,p1))

 proof

 per cases ;

 suppose

 A68: ( angle (p1,p4,p2)) = 0 ;

 then ( angle (p2,p4,p1)) = 0 by EUCLID_3: 36;

 hence thesis by A67, A68, EUCLID_3: 36;

 end;

 suppose

 A69: ( angle (p1,p4,p2)) <> 0 ;

 then ( angle (p2,p4,p1)) = ((2 * PI ) - ( angle (p1,p4,p2))) by EUCLID_3: 37;

 hence thesis by A67, A69, EUCLID_3: 37;

 end;

 end;

 then

 A70: ( angle (p2,p4,p1)) = ( angle (p2,p3,p5)) by A38, A44, Th10;



 A71: ( angle (p4,p1,p2)) = ( angle (p3,p5,p2))

 proof



 A72: ( euc2cpx p2) <> ( euc2cpx p5) & ( euc2cpx p3) <> ( euc2cpx p5) by A44, A51, EUCLID_3: 4;



 A73: ( euc2cpx p4) <> ( euc2cpx p1) & ( euc2cpx p2) <> ( euc2cpx p3) by A28, A32, EUCLID_3: 4;



 A74: ( euc2cpx p2) <> ( euc2cpx p4) & ( euc2cpx p2) <> ( euc2cpx p1) by A26, A24, EUCLID_3: 4;

 per cases by A74, A73, A72, COMPLEX2: 88;

 suppose ((( angle (p2,p4,p1)) + ( angle (p4,p1,p2))) + ( angle (p1,p2,p4))) = PI & ((( angle (p2,p3,p5)) + ( angle (p3,p5,p2))) + ( angle (p5,p2,p3))) = PI or ((( angle (p2,p4,p1)) + ( angle (p4,p1,p2))) + ( angle (p1,p2,p4))) = (5 * PI ) & ((( angle (p2,p3,p5)) + ( angle (p3,p5,p2))) + ( angle (p5,p2,p3))) = (5 * PI );

 hence thesis by A70, A48;

 end;

 suppose

 A75: ((( angle (p2,p4,p1)) + ( angle (p4,p1,p2))) + ( angle (p1,p2,p4))) = (5 * PI ) & ((( angle (p2,p3,p5)) + ( angle (p3,p5,p2))) + ( angle (p5,p2,p3))) = PI ;

 ( angle (p4,p1,p2)) < (2 * PI ) & ( angle (p3,p5,p2)) >= 0 by COMPLEX2: 70;

 then

 A76: (( angle (p4,p1,p2)) - ( angle (p3,p5,p2))) < ((2 * PI ) - 0 ) by XREAL_1: 14;

 (( angle (p4,p1,p2)) - ( angle (p3,p5,p2))) = (4 * PI ) by A70, A48, A75;

 hence thesis by A76, XREAL_1: 64;

 end;

 suppose

 A77: ((( angle (p2,p4,p1)) + ( angle (p4,p1,p2))) + ( angle (p1,p2,p4))) = PI & ((( angle (p2,p3,p5)) + ( angle (p3,p5,p2))) + ( angle (p5,p2,p3))) = (5 * PI );

 ( angle (p3,p5,p2)) < (2 * PI ) & ( angle (p4,p1,p2)) >= 0 by COMPLEX2: 70;

 then

 A78: (( angle (p3,p5,p2)) - ( angle (p4,p1,p2))) < ((2 * PI ) - 0 ) by XREAL_1: 14;

 (( angle (p3,p5,p2)) - ( angle (p4,p1,p2))) = (4 * PI ) by A70, A48, A77;

 hence thesis by A78, XREAL_1: 64;

 end;

 end;

 (p2,p3,p5) are_mutually_distinct by A32, A44, A51, ZFMISC_1:def 5;

 then (p2,p3,p5) is_a_triangle by A70, A48, A71, A30, A29, A27, Th20;

 then ( |.(p5 - p3).| * |.(p4 - p2).|) = ( |.(p3 - p2).| * |.(p1 - p4).|) by A70, A48, A31, Th21;

 then ( |.(p5 - p3).| * |.(p4 - p2).|) = ( |.(p3 - p2).| * |.(p4 - p1).|) by Lm2;

 then

 A79: ( |.(p3 - p5).| * |.(p4 - p2).|) = ( |.(p3 - p2).| * |.(p4 - p1).|) by Lm2;

 (p4,p2,p3) are_mutually_distinct by A32, A24, A22, ZFMISC_1:def 5;

 then

 A80: (p4,p2,p3) is_a_triangle by A40, A34, A25, Th20;



 A81: |.(p3 - p1).| = ( sqrt ( |.(p3 - p1).| ^2 )) by SQUARE_1: 22

 .= ( sqrt ((( |.(p1 - p5).| ^2 ) + ( |.(p3 - p5).| ^2 )) - (((2 * |.(p1 - p5).|) * |.(p3 - p5).|) * ( cos ( angle (p1,p5,p3)))))) by Th7

 .= ( sqrt ((( |.(p1 - p5).| ^2 ) + ( |.(p3 - p5).| ^2 )) - (((2 * |.(p1 - p5).|) * |.(p3 - p5).|) * ( cos PI )))) by A38, A43, A44, Th8

 .= ( sqrt (( |.(p1 - p5).| + |.(p3 - p5).|) ^2 )) by SIN_COS: 77

 .= ( |.(p1 - p5).| + |.(p3 - p5).|) by SQUARE_1: 22;

 ( angle (p5,p1,p2)) <> PI by A2, A3, A4, A24, A22, A38, A43, A56, Th9, Th35;

 then (p1,p2,p5) is_a_triangle by A34, A60, A41, A54, Th20;

 then ( |.(p1 - p5).| * |.(p2 - p4).|) = ( |.(p2 - p1).| * |.(p4 - p3).|) by A47, A39, A59, A80, Th21;

 then ( |.(p1 - p5).| * |.(p4 - p2).|) = ( |.(p2 - p1).| * |.(p4 - p3).|) by Lm2;



 hence (( |.(p2 - p1).| * |.(p4 - p3).|) + ( |.(p3 - p2).| * |.(p4 - p1).|)) = (( |.(p5 - p1).| * |.(p4 - p2).|) + ( |.(p3 - p5).| * |.(p4 - p2).|)) by A79, Lm2

 .= (( |.(p5 - p1).| + |.(p3 - p5).|) * |.(p4 - p2).|)

 .= ( |.(p3 - p1).| * |.(p4 - p2).|) by A81, Lm2;

 end;

 end;

 begin

 reserve c1,c2,c3 for Element of COMPLEX ;

 theorem :: EUCLID_6:41

 ((p1 - p2) `1 ) = ((p1 `1 ) - (p2 `1 )) & ((p1 - p2) `2 ) = ((p1 `2 ) - (p2 `2 )) by Lm15;

 theorem :: EUCLID_6:42

 |.(p1 - p2).| = 0 iff p1 = p2 by Lm1;

 theorem :: EUCLID_6:43

 |.(p1 - p2).| = |.(p2 - p1).| by Lm2;

 theorem :: EUCLID_6:44

 not ( angle (p1,p2,p3)) = ((2 * ( angle (p4,p5,p6))) + (2 * PI )) by Lm3;

 theorem :: EUCLID_6:45

 not ( angle (p1,p2,p3)) = ((2 * ( angle (p4,p5,p6))) + (4 * PI )) by Lm4;

 theorem :: EUCLID_6:46

 not ( angle (p1,p2,p3)) = ((2 * ( angle (p4,p5,p6))) - (4 * PI )) by Lm5;

 theorem :: EUCLID_6:47

 not ( angle (p1,p2,p3)) = ((2 * ( angle (p4,p5,p6))) - (6 * PI )) by Lm6;

 theorem :: EUCLID_6:48

 c1 = ( euc2cpx (p1 - p2)) & c2 = ( euc2cpx (p3 - p2)) implies ( angle (p1,p2,p3)) = ( angle (c1,c2)) by Lm7;

 theorem :: EUCLID_6:49

 (( angle (c1,c2)) + ( angle (c2,c3))) = ( angle (c1,c3)) or (( angle (c1,c2)) + ( angle (c2,c3))) = (( angle (c1,c3)) + (2 * PI )) by Lm14;

 theorem :: EUCLID_6:50

 c1 = ( euc2cpx (p1 - p2)) & c2 = ( euc2cpx (p3 - p2)) implies ( Re (c1 .|. c2)) = ((((p1 `1 ) - (p2 `1 )) * ((p3 `1 ) - (p2 `1 ))) + (((p1 `2 ) - (p2 `2 )) * ((p3 `2 ) - (p2 `2 )))) & ( Im (c1 .|. c2)) = (( - (((p1 `1 ) - (p2 `1 )) * ((p3 `2 ) - (p2 `2 )))) + (((p1 `2 ) - (p2 `2 )) * ((p3 `1 ) - (p2 `1 )))) & |.c1.| = ( sqrt ((((p1 `1 ) - (p2 `1 )) ^2 ) + (((p1 `2 ) - (p2 `2 )) ^2 ))) & |.(p1 - p2).| = |.c1.| by Lm16;

 theorem :: EUCLID_6:51

 for n be Element of NAT , q1 be Point of ( TOP-REAL n) holds for f be Function of ( TOP-REAL n), R^1 st (for q be Point of ( TOP-REAL n) holds (f . q) = |.(q - q1).|) holds f is continuous by Lm20;

 theorem :: EUCLID_6:52

 for n be Element of NAT , q1 be Point of ( TOP-REAL n) holds ex f be Function of ( TOP-REAL n), R^1 st (for q be Point of ( TOP-REAL n) holds (f . q) = |.(q - q1).|) & f is continuous by Lm21;