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 & angle p1,p2,p3 = 0 & p1 <> p2 & p2 <> p3 holds
p1 = p3
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 & 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:6;
assume A5: p1 <> p3 ; :: thesis: contradiction
then euc2cpx p1 <> euc2cpx p3 by EUCLID_3:6;
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:101;
hence contradiction by A1, A3, A5, Th35; :: thesis: verum