theorem Th41: :: COMPTRIG:41

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