let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis:
assume that
A1: ( p2 <> p1 & p1 <> p3 ) and
A2: p3 <> p2 and
A3: angle (p2,p1,p3) < PI ; :: thesis:
A4: ( euc2cpx p1 <> euc2cpx p2 & euc2cpx p1 <> euc2cpx p3 ) by A1, Th4;
A5: euc2cpx p3 <> euc2cpx p2 by A2, Th4;

per cases by COMPLEX2:70;

suppose A6: 0 = angle ((euc2cpx p2),(euc2cpx p1),(euc2cpx p3)) ; :: thesis:

now :: thesis:

per cases by A4, A5, A6, COMPLEX2:87;

suppose ( angle ((euc2cpx p1),(euc2cpx p3),(euc2cpx p2)) = 0 & angle ((euc2cpx p3),(euc2cpx p2),(euc2cpx p1)) = PI ) ; :: thesis:

hence ((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI by A6; :: thesis:

end;

suppose ( angle ((euc2cpx p1),(euc2cpx p3),(euc2cpx p2)) = PI & angle ((euc2cpx p3),(euc2cpx p2),(euc2cpx p1)) = 0 ) ; :: thesis:

hence ((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI by A6; :: thesis:

end;

end;

end;

hence ((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI ; :: thesis:

end;

suppose 0 < angle ((euc2cpx p2),(euc2cpx p1),(euc2cpx p3)) ; :: thesis:

hence ((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI by A3, A4, COMPLEX2:84; :: thesis:

end;

end;