theorem Th13: :: COMPLEX2:15

for z being Complex holds
( Arg z = 0 iff z = |.z.| )