let p1, p2, p3 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 & p1 <> p2 & p2 <> p3 holds
angle p1,p2,p3 <> PI
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 & 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