:: deftheorem Def3 defines angle COMPLEX2:def 3 :
for a, b being Complex holds
( ( ( Arg a = 0 or b <> 0 ) implies angle (a,b) = Arg (Rotate (b,(- (Arg a)))) ) & ( Arg a = 0 or b <> 0 or angle (a,b) = (2 * PI) - (Arg a) ) );