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) & angle (p1,p2,p3) = 0 & p1 <> p2 & p2 <> p3 holds
p1 = p3
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) & angle (p1,p2,p3) = 0 & p1 <> p2 & p2 <> p3 implies p1 = p3 )
assume A1: ( p1 in circle (a,b,r) & p2 in circle (a,b,r) & p3 in circle (a,b,r) ) ; :: thesis: ( not angle (p1,p2,p3) = 0 or not p1 <> p2 or not p2 <> p3 or p1 = p3 )
assume A2: angle (p1,p2,p3) = 0 ; :: thesis: ( not p1 <> p2 or not p2 <> p3 or p1 = p3 )
assume A3: ( p1 <> p2 & p2 <> p3 ) ; :: thesis: p1 = p3
then A4: ( euc2cpx p1 <> euc2cpx p2 & euc2cpx p2 <> euc2cpx p3 ) by EUCLID_3:4;
assume A5: p1 <> p3 ; :: thesis: contradiction
then euc2cpx p1 <> euc2cpx p3 by EUCLID_3:4;
then ( ( angle (p2,p3,p1) = 0 & angle (p3,p1,p2) = PI ) or ( angle (p2,p3,p1) = PI & angle (p3,p1,p2) = 0 ) ) by A2, A4, COMPLEX2:87;
hence contradiction by A1, A3, A5, Th35; :: thesis: verum