let p1, p2, p3, p4, p be Point of (TOP-REAL 2); :: thesis: for a, b, r being Real 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_distinct holds
angle (p1,p4,p2) = angle (p1,p3,p2)
let a, b, r be Real; :: 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_distinct implies angle (p1,p4,p2) = angle (p1,p3,p2) )
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) ; :: thesis: ( not p in LSeg (p1,p3) or not p in LSeg (p2,p4) or not p1,p2,p3,p4 are_mutually_distinct or angle (p1,p4,p2) = angle (p1,p3,p2) )
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) ; :: thesis: ( not p1,p2,p3,p4 are_mutually_distinct or angle (p1,p4,p2) = angle (p1,p3,p2) )
assume A8: p1,p2,p3,p4 are_mutually_distinct ; :: thesis: angle (p1,p4,p2) = angle (p1,p3,p2)
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 ) ; :: thesis: contradiction

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

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

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; :: thesis: verum

end;

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

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; :: thesis: verum

end;

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 ) ; :: thesis: contradiction

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

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

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; :: thesis: verum

end;

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

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; :: thesis: verum

end;

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 ( 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, A2, A3, A4, A13, A11, A23, A12, 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 A32: 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: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 angle (p1,p4,p2) = angle (p1,p3,p2) by XBOOLE_0:def 7; :: thesis: verum

end;

suppose A36: 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: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 angle (p1,p4,p2) = angle (p1,p3,p2) by XBOOLE_0:def 7; :: thesis: verum

end;

end;