for z being Complex holds
( Arg z in ].0,PI.[ iff Im z > 0 )