theorem Th21: :: COMPLEX2:23

for z being Complex holds
( Im z = 0 iff ( Arg z = 0 or Arg z = PI ) )