let p1, p2, p3, p4, p 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 & 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_different holds
angle p1,p4,p2 = angle p1,p3,p2
let a, b, r be real number ; :: thesis: ( 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_different implies angle p1,p4,p2 = angle p1,p3,p2 )
assume A1: ( p1 in circle a,b,r & p2 in circle a,b,r & p3 in circle a,b,r & p4 in circle a,b,r ) ; :: thesis: ( not p in LSeg p1,p3 or not p in LSeg p2,p4 or not p1,p2,p3,p4 are_mutually_different or angle p1,p4,p2 = angle p1,p3,p2 )
assume A2: ( p in LSeg p1,p3 & p in LSeg p2,p4 ) ; :: thesis: ( not p1,p2,p3,p4 are_mutually_different or angle p1,p4,p2 = angle p1,p3,p2 )
assume p1,p2,p3,p4 are_mutually_different ; :: thesis: angle p1,p4,p2 = angle p1,p3,p2
then A3: ( p1 <> p2 & p1 <> p3 & p1 <> p4 & p2 <> p3 & p2 <> p4 & p3 <> p4 ) by ZFMISC_1:def 6;
A4: inside_of_circle a,b,r misses circle a,b,r by TOPREAL9:54;
A5: (LSeg p2,p4) \ {p2,p4} c= inside_of_circle a,b,r by A1, TOPREAL9:60;
A6: (LSeg p1,p3) \ {p1,p3} c= inside_of_circle a,b,r by A1, TOPREAL9:60;
A7: ( p <> p1 & p <> p4 )

proof

assume A8: ( p = p1 or p = p4 ) ; :: thesis: contradiction

per cases ( p = p1 or p = p4 ) by A8;

suppose A9: p = p1 ; :: thesis: contradiction

not p1 in {p2,p4} by A3, TARSKI:def 2;
then p1 in (LSeg p2,p4) \ {p2,p4} by A2, A9, XBOOLE_0:def 5;
then p1 in (inside_of_circle a,b,r) /\ (circle a,b,r) by A1, A5, XBOOLE_0:def 4;
hence contradiction by A4, XBOOLE_0:def 7; :: thesis: verum

end;

suppose A10: p = p4 ; :: thesis: contradiction

not p4 in {p1,p3} by A3, TARSKI:def 2;
then p4 in (LSeg p1,p3) \ {p1,p3} by A2, A10, XBOOLE_0:def 5;
then p4 in (inside_of_circle a,b,r) /\ (circle a,b,r) by A1, A6, XBOOLE_0:def 4;
hence contradiction by A4, XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

A11: ( p <> p2 & p <> p3 )

proof

assume A12: ( p = p2 or p = p3 ) ; :: thesis: contradiction

per cases ( p = p3 or p = p2 ) by A12;

suppose A13: p = p3 ; :: thesis: contradiction

not p3 in {p2,p4} by A3, TARSKI:def 2;
then p3 in (LSeg p2,p4) \ {p2,p4} by A2, A13, XBOOLE_0:def 5;
then p3 in (inside_of_circle a,b,r) /\ (circle a,b,r) by A1, A5, XBOOLE_0:def 4;
hence contradiction by A4, XBOOLE_0:def 7; :: thesis: verum

end;

suppose A14: p = p2 ; :: thesis: contradiction

not p2 in {p1,p3} by A3, TARSKI:def 2;
then p2 in (LSeg p1,p3) \ {p1,p3} by A2, A14, XBOOLE_0:def 5;
then p2 in (inside_of_circle a,b,r) /\ (circle a,b,r) by A1, A6, XBOOLE_0:def 4;
hence contradiction by A4, XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

A15: angle p1,p4,p = angle p1,p4,p2 by A2, A7, Th10;
A16: angle p,p3,p2 = angle p1,p3,p2 by A2, A11, Th9;
A17: angle p4,p,p1 = angle p2,p,p3 by A2, A7, A11, Th15;
A18: p1,p4,p are_mutually_different by A3, A7, ZFMISC_1:def 5;
A19: p2,p,p3 are_mutually_different by A3, A11, ZFMISC_1:def 5;
A20: p,p3,p2 are_mutually_different by A3, A11, ZFMISC_1:def 5;
A21: p4,p,p1 are_mutually_different by A3, A7, ZFMISC_1:def 5;

per cases ( angle p1,p4,p2 = angle p1,p3,p2 or angle p1,p4,p2 = (angle p1,p3,p2) - PI or angle p1,p4,p2 = (angle p1,p3,p2) + PI ) by A1, A3, Th34;

suppose angle p1,p4,p2 = angle p1,p3,p2 ; :: thesis: angle p1,p4,p2 = angle p1,p3,p2

hence angle p1,p4,p2 = angle p1,p3,p2 ; :: thesis: verum

end;

suppose A22: angle p1,p4,p2 = (angle p1,p3,p2) - PI ; :: thesis: angle p1,p4,p2 = angle p1,p3,p2

angle p1,p3,p2 < 2 * PI by COMPLEX2:84;
then (angle p1,p3,p2) - PI < (2 * PI ) - PI by XREAL_1:11;
then angle p2,p,p3 <= PI by A15, A17, A18, A22, Th23;
then A23: angle p1,p3,p2 <= PI by A16, A19, Th23;
angle p1,p4,p2 >= 0 by COMPLEX2:84;
then ((angle p1,p3,p2) - PI ) + PI >= 0 + PI by A22, XREAL_1:8;
then A24: p3 in LSeg p1,p2 by A23, Th11, XXREAL_0:1;
A25: (LSeg p1,p2) \ {p1,p2} c= inside_of_circle a,b,r by A1, TOPREAL9:60;
A26: inside_of_circle a,b,r misses circle a,b,r by TOPREAL9:54;
not p3 in {p1,p2} by A3, TARSKI:def 2;
then p3 in (LSeg p1,p2) \ {p1,p2} by A24, XBOOLE_0:def 5;
then p3 in (inside_of_circle a,b,r) /\ (circle a,b,r) by A1, A25, XBOOLE_0:def 4;
hence angle p1,p4,p2 = angle p1,p3,p2 by A26, XBOOLE_0:def 7; :: thesis: verum

end;

suppose A27: angle p1,p4,p2 = (angle p1,p3,p2) + PI ; :: thesis: angle p1,p4,p2 = angle p1,p3,p2

angle p1,p4,p2 < 2 * PI by COMPLEX2:84;
then (angle p1,p4,p2) - PI < (2 * PI ) - PI by XREAL_1:11;
then angle p4,p,p1 <= PI by A16, A17, A20, A27, Th23;
then A28: angle p1,p4,p2 <= PI by A15, A21, Th23;
angle p1,p3,p2 >= 0 by COMPLEX2:84;
then ((angle p1,p4,p2) - PI ) + PI >= 0 + PI by A27, XREAL_1:8;
then A29: p4 in LSeg p1,p2 by A28, Th11, XXREAL_0:1;
A30: (LSeg p1,p2) \ {p1,p2} c= inside_of_circle a,b,r by A1, TOPREAL9:60;
A31: inside_of_circle a,b,r misses circle a,b,r by TOPREAL9:54;
not p4 in {p1,p2} by A3, TARSKI:def 2;
then p4 in (LSeg p1,p2) \ {p1,p2} by A29, XBOOLE_0:def 5;
then p4 in (inside_of_circle a,b,r) /\ (circle a,b,r) by A1, A30, XBOOLE_0:def 4;
hence angle p1,p4,p2 = angle p1,p3,p2 by A31, XBOOLE_0:def 7; :: thesis: verum

end;

end;