let a, b, c be 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 Th68; :: thesis: verum