let a, b, c be Element of COMPLEX ; :: thesis: ( angle (a,b,c) = PI implies angle (c,b,a) = PI )
assume A1: angle (a,b,c) = PI ; :: thesis: angle (c,b,a) = PI
then (angle (a,b,c)) + (angle (c,b,a)) = 0 + (2 * PI) by Th94, COMPTRIG:21;
hence angle (c,b,a) = PI by A1; :: thesis: verum