let p1, p2, p3 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) & p1 <> p2 & p2 <> p3 holds
angle (p1,p2,p3) <> PI
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) & p1 <> p2 & p2 <> p3 implies angle (p1,p2,p3) <> PI )
assume A1: p1 in circle (a,b,r) ; :: thesis: ( not p2 in circle (a,b,r) or not p3 in circle (a,b,r) or not p1 <> p2 or not p2 <> p3 or angle (p1,p2,p3) <> PI )
assume A2: p2 in circle (a,b,r) ; :: thesis: ( not p3 in circle (a,b,r) or not p1 <> p2 or not p2 <> p3 or angle (p1,p2,p3) <> PI )
assume p3 in circle (a,b,r) ; :: thesis: ( not p1 <> p2 or not p2 <> p3 or angle (p1,p2,p3) <> PI )
then A3: (LSeg (p1,p3)) \ {p1,p3} c= inside_of_circle (a,b,r) by A1, TOPREAL9:60;
assume ( p1 <> p2 & p2 <> p3 ) ; :: thesis: angle (p1,p2,p3) <> PI
then A4: not p2 in {p1,p3} by TARSKI:def 2;
inside_of_circle (a,b,r) misses circle (a,b,r) by TOPREAL9:54;
then A5: (inside_of_circle (a,b,r)) /\ (circle (a,b,r)) = {} by XBOOLE_0:def 7;
assume angle (p1,p2,p3) = PI ; :: thesis: contradiction
then p2 in LSeg (p1,p3) by Th11;
then p2 in (LSeg (p1,p3)) \ {p1,p3} by A4, XBOOLE_0:def 5;
hence contradiction by A2, A3, A5, XBOOLE_0:def 4; :: thesis: verum