theorem :: COMPLEX1:47

for z being Complex holds
( z <> 0 iff 0 < |.z.| ) ;