theorem :: COMPLEX3:22

for a, b being non zero Real holds ((a / b) + (b / a)) |^ 2 >= 4