let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( angle (p3,p2,p1) <> 0 implies angle (p3,p2,p1) = (2 * PI) - (angle (p1,p2,p3)) )
assume angle (p3,p2,p1) <> 0 ; :: thesis: angle (p3,p2,p1) = (2 * PI) - (angle (p1,p2,p3))
then (angle (p3,p2,p1)) + (angle (p1,p2,p3)) = 2 * PI by COMPLEX2:80;
hence angle (p3,p2,p1) = (2 * PI) - (angle (p1,p2,p3)) ; :: thesis: verum