theorem :: COMPLEX3:16

for a, b being Real st a * b is negative holds
|.(a - b).| > |.(a + b).|