theorem Th43: :: COMPTRIG:43

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