theorem :: XCMPLX_1:151

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