theorem Th16: :: COMPLEX2:18

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