theorem :: XCMPLX_1:138

for a, b being Complex holds a = ((- b) + a) + b ;