theorem :: COMPLEX1:46

for z being Complex holds 0 <= |.z.| ;