theorem Th19: :: COMPLEX2:21
for z being Complex holds
( Arg z = 0 iff ( Re z >= 0 & Im z = 0 ) )