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]| & p1 <> p & p2 <> 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]| & p1 <> p & p2 <> 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 p1 <> p or not p2 <> 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 p1 <> p or not p2 <> 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 p1 <> p or not p2 <> p or 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 )
assume A4: pc = |[a,b]| ; :: thesis: ( not p1 <> p or not p2 <> p or 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 )
assume that
A5: p1 <> p and
A6: p2 <> 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 )

A11: |.(p2 - pc).| = r by A2, A4, TOPREAL9:43;
|.(p1 - pc).| >= 0 ;
then r > 0 by A1, A4, A10, TOPREAL9:43;
then consider p3 being Point of (TOP-REAL 2) 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 ( p2 = p3 or p2 <> p3 ) ;

suppose p2 = p3 ; :: 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 ) by A1, A3, A4, A5, A12, A13, Th31; :: thesis: verum

end;

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

A15: angle p2,pc,p3 <> 0

proof

set z3 = euc2cpx (p3 - pc);
set z2 = euc2cpx (p2 - pc);
assume angle p2,pc,p3 = 0 ; :: thesis: contradiction
then A16: Arg (p2 - pc) = Arg (p3 - pc) by EUCLID_3:45;
A17: |.(p2 - pc).| = |.(p3 - pc).| by A4, A11, A12, TOPREAL9:43;
A18: |.(euc2cpx (p2 - pc)).| = |.(p2 - pc).| by EUCLID_3:31
.= |.(euc2cpx (p3 - pc)).| by A17, EUCLID_3:31 ;
A19: euc2cpx (p2 - pc) = (|.(euc2cpx (p2 - pc)).| * (cos (Arg (euc2cpx (p2 - pc))))) + ((|.(euc2cpx (p2 - pc)).| * (sin (Arg (euc2cpx (p2 - pc))))) * <i> ) by COMPLEX2:19
.= euc2cpx (p3 - pc) by A16, A18, COMPLEX2:19 ;
p2 = p2 + (0. (TOP-REAL 2)) by EUCLID:31
.= p2 + (pc + (- pc)) by EUCLID:40
.= (p2 + (- pc)) + pc by EUCLID:30
.= (p3 - pc) + pc by A19, EUCLID_3:6
.= p3 + (pc + (- pc)) by EUCLID:30
.= p3 + (0. (TOP-REAL 2)) by EUCLID:40
.= p3 by EUCLID:31 ;
hence contradiction by A14; :: thesis: verum

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:84;
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 ; :: thesis: 2 * (angle p3,p,p2) = angle p3,pc,p2
thus 2 * (angle p3,p,p2) = 2 * ((2 * PI ) - (angle p2,p,p3)) by A20, EUCLID_3:46
.= (2 * PI ) - (2 * ((angle p2,p,p3) - PI ))
.= angle p3,pc,p2 by A15, A22, EUCLID_3:46 ; :: thesis: verum

end;

A23: angle p3,p,p2 = (2 * PI ) - (angle p2,p,p3) by A20, EUCLID_3:46;
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 ; :: thesis: 2 * ((angle p3,p,p2) - PI ) = angle p3,pc,p2
hence 2 * ((angle p3,p,p2) - PI ) = (2 * PI ) - (angle p2,pc,p3) by A23
.= angle p3,pc,p2 by A15, EUCLID_3:46 ;
:: thesis: verum

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 ( angle p1,pc,p2 = (angle p1,pc,p3) + (angle p3,pc,p2) or (angle p1,pc,p2) + (2 * PI ) = (angle p1,pc,p3) + (angle p3,pc,p2) ) by Th4;

suppose A26: angle p1,pc,p2 = (angle p1,pc,p3) + (angle p3,pc,p2) ; :: thesis: ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 )

per cases ( ( 2 * (angle p1,p,p3) = angle p1,pc,p3 & 2 * ((angle p3,p,p2) - PI ) = angle p3,pc,p2 ) or ( 2 * (angle p1,p,p3) = angle p1,pc,p3 & 2 * (angle p3,p,p2) = angle p3,pc,p2 ) or ( 2 * ((angle p1,p,p3) - PI ) = angle p1,pc,p3 & 2 * ((angle p3,p,p2) - PI ) = angle p3,pc,p2 ) or ( 2 * ((angle p1,p,p3) - PI ) = angle p1,pc,p3 & 2 * (angle p3,p,p2) = angle p3,pc,p2 ) ) 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 ) ; :: thesis: ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,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 ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 ) by Lm3; :: thesis: verum

end;

suppose ( 2 * (angle p1,p,p3) = angle p1,pc,p3 & 2 * (angle p3,p,p2) = angle p3,pc,p2 ) ; :: thesis: ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,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 ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 ) by Lm4; :: thesis: verum

end;

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

then angle p1,pc,p2 = (2 * ((angle p1,p,p3) + (angle p3,p,p2))) - (4 * PI ) by A26;
hence ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 ) by A25, Lm5; :: thesis: verum

end;

suppose ( 2 * ((angle p1,p,p3) - PI ) = angle p1,pc,p3 & 2 * (angle p3,p,p2) = angle p3,pc,p2 ) ; :: thesis: ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,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 ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 ) by Lm3; :: thesis: verum

end;

end;

end;

suppose A27: (angle p1,pc,p2) + (2 * PI ) = (angle p1,pc,p3) + (angle p3,pc,p2) ; :: thesis: ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 )

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

then angle p1,pc,p2 = (2 * ((angle p1,p,p3) + (angle p3,p,p2))) - (4 * PI ) by A27;
hence ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 ) by A25, Lm5; :: thesis: verum

end;

suppose ( 2 * (angle p1,p,p3) = angle p1,pc,p3 & 2 * (angle p3,p,p2) = angle p3,pc,p2 ) ; :: thesis: ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,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 ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 ) by Lm3; :: thesis: verum

end;

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

then angle p1,pc,p2 = (2 * ((angle p1,p,p3) + (angle p3,p,p2))) - (6 * PI ) by A27;
hence ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 ) by A25, Lm6; :: thesis: verum

end;

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

then angle p1,pc,p2 = (2 * ((angle p1,p,p3) + (angle p3,p,p2))) - (4 * PI ) by A27;
hence ( 2 * (angle p1,p,p2) = angle p1,pc,p2 or 2 * ((angle p1,p,p2) - PI ) = angle p1,pc,p2 ) by A25, Lm5; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;