theorem Th44: :: COMPTRIG:44

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