let a, b, c be Element of COMPLEX ; :: thesis: ( angle a,b,c <> 0 iff (angle a,b,c) + (angle c,b,a) = 2 * PI )

hereby :: thesis: ( (angle a,b,c) + (angle c,b,a) = 2 * PI implies angle a,b,c <> 0 )

assume angle a,b,c <> 0 ; :: thesis: (angle a,b,c) + (angle c,b,a) = 2 * PI
then angle c,b,a = (2 * PI ) - (angle a,b,c) by Lm4;
hence (angle a,b,c) + (angle c,b,a) = 2 * PI ; :: thesis: verum

end;

assume ( (angle a,b,c) + (angle c,b,a) = 2 * PI & angle a,b,c = 0 ) ; :: thesis: contradiction
hence contradiction by Th84; :: thesis: verum