let p1, p3, p4, p be Point of (TOP-REAL 2); :: thesis:
let a, b, r be real number ; :: thesis:
assume A1: p1 in circle a,b,r ; :: thesis:
assume A2: p3 in circle a,b,r ; :: thesis:
assume A3: p4 in circle a,b,r ; :: thesis:
assume A4: p in LSeg p1,p3 ; :: thesis:
assume A5: p in LSeg p1,p4 ; :: thesis:
assume A6: p3 <> p4 ; :: thesis:

per cases ;

suppose A7: ( p1 = p3 or p1 = p4 ) ; :: thesis:

per cases by A7;

suppose p1 = p3 ; :: thesis:

then p in {p1} by A4, RLTOPSP1:71;
hence p = p1 by TARSKI:def 1; :: thesis:

end;

suppose p1 = p4 ; :: thesis:

then p in {p1} by A5, RLTOPSP1:71;
hence p = p1 by TARSKI:def 1; :: thesis:

end;

end;

end;

suppose A8: ( p1 <> p3 & p1 <> p4 ) ; :: thesis:

per cases ;

suppose A9: p <> p1 ; :: thesis:

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

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 p = p1 by A10, XBOOLE_0:def 7; :: thesis:

end;

suppose A13: p4 in LSeg p1,p3 ; :: thesis:

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 p = p1 by A10, XBOOLE_0:def 7; :: thesis:

end;

end;

end;

suppose p = p1 ; :: thesis:

hence p = p1 ; :: thesis:

end;

end;

end;

end;