let p1, p2, p, pc be Point of (TOP-REAL 2); :: thesis: for a, b, r being real number st 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 & not 2 * (angle p1,p,p2) = angle p1,pc,p2 holds
2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2
let a, b, r be real number ; :: thesis: ( 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 & not 2 * (angle p1,p,p2) = angle p1,pc,p2 implies 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 )
assume A1: p1 in circle a,b,r ; :: thesis: ( not p2 in circle a,b,r or not p in circle a,b,r or not pc = |[a,b]| or not pc in LSeg p,p2 or not p1 <> p or 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 )
assume A2: p2 in circle a,b,r ; :: thesis: ( not p in circle a,b,r or not pc = |[a,b]| or not pc in LSeg p,p2 or not p1 <> p or 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 )
assume A3: p in circle a,b,r ; :: thesis: ( not pc = |[a,b]| or not pc in LSeg p,p2 or not p1 <> p or 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 )
assume that
A4: pc = |[a,b]| and
A5: pc in LSeg p,p2 ; :: thesis: ( not p1 <> p or 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 )
assume A6: p1 <> p ; :: thesis: ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 )

per cases ( r = 0 or r <> 0 ) ;

suppose A7: r = 0 ; :: thesis: ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 )

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:93
.= angle pc,pc,pc by COMPLEX2:93 ;
hence ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 ) by A9, A8, Lm1; :: thesis: verum

end;

suppose A10: r <> 0 ; :: thesis: ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 )

|.(p2 - pc).| = r by A2, A4, TOPREAL9:43;
then A11: pc <> p2 by A10, Lm1;
A12: euc2cpx p1 <> euc2cpx p by A6, EUCLID_3:6;
A13: |.(p1 - pc).| = r by A1, A4, TOPREAL9:43;
then pc <> p1 by A10, Lm1;
then A14: euc2cpx pc <> euc2cpx p1 by EUCLID_3:6;
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:6;
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:102;

per cases ( ( (angle p,pc,p1) + (angle p1,pc,p2) = PI & (2 * (angle p1,p,p2)) + (angle p,pc,p1) = PI ) or ( (angle p,pc,p1) + (angle p1,pc,p2) = 3 * PI & (2 * (angle p1,p,p2)) + (angle p,pc,p1) = PI ) or ( (angle p,pc,p1) + (angle p1,pc,p2) = PI & (2 * (angle p1,p,p2)) + (angle p,pc,p1) = 5 * PI ) or ( (angle p,pc,p1) + (angle p1,pc,p2) = 3 * PI & (2 * (angle p1,p,p2)) + (angle p,pc,p1) = 5 * PI ) ) 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 ) ; :: thesis: ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 )

hence ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 ) ; :: thesis: verum

end;

suppose A20: ( (angle p,pc,p1) + (angle p1,pc,p2) = 3 * PI & (2 * (angle p1,p,p2)) + (angle p,pc,p1) = PI ) ; :: thesis: ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 )

( angle p1,pc,p2 < 2 * PI & angle p1,p,p2 >= 0 ) by COMPLEX2:84;
then (- (2 * (angle p1,p,p2))) + (angle p1,pc,p2) < 0 + (2 * PI ) by XREAL_1:10;
hence ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 ) by A20; :: thesis: verum

end;

suppose A21: ( (angle p,pc,p1) + (angle p1,pc,p2) = PI & (2 * (angle p1,p,p2)) + (angle p,pc,p1) = 5 * PI ) ; :: thesis: ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 )

( angle p1,pc,p2 >= 0 & (angle p1,p,p2) * 2 < (2 * PI ) * 2 ) by COMPLEX2:84, XREAL_1:70;
then (2 * (angle p1,p,p2)) + (- (angle p1,pc,p2)) < ((2 * PI ) * 2) + 0 by XREAL_1:10;
hence ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 ) by A21; :: thesis: verum

end;

suppose ( (angle p,pc,p1) + (angle p1,pc,p2) = 3 * PI & (2 * (angle p1,p,p2)) + (angle p,pc,p1) = 5 * PI ) ; :: thesis: ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 )

hence ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 ) ; :: thesis: verum

end;

end;

end;

end;