let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( angle p1,p2,p3 <> 0 implies angle p3,p2,p1 = (2 * PI ) - (angle p1,p2,p3) )
assume angle p1,p2,p3 <> 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:94;
hence angle p3,p2,p1 = (2 * PI ) - (angle p1,p2,p3) ; :: thesis: verum