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