theorem Th42: :: COMPTRIG:42

for z being Complex holds
( Arg z in ].(PI / 2),PI.[ iff ( Re z < 0 & Im z > 0 ) )