for z being Complex holds
( Arg z = PI iff ( Re z < 0 & Im z = 0 ) )