theorem :: XCMPLX_1:183

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