for z being Complex holds
( 0 <= Arg z & Arg z < 2 * PI )