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