theorem :: XCMPLX_1:186

for a being Complex holds a - (2 * a) = - a ;