theorem Th12: :: COMPLEX2:13

for z being Complex st z <> 0 holds
( ( Arg z < PI implies Arg (- z) = (Arg z) + PI ) & ( Arg z >= PI implies Arg (- z) = (Arg z) - PI ) )