theorem :: COMPLEX1:79

for a, b being Real holds |.a.| <= sqrt ((a ^2) + (b ^2))