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