theorem :: COMPLEX3:17

for a, b being non zero Real holds |.((a |^ 2) - (b |^ 2)).| < |.((a |^ 2) + (b |^ 2)).|