theorem Th13: :: COMSEQ_3:13

for z being Complex holds
( |.(Re z).| <= |.z.| & |.(Im z).| <= |.z.| )