theorem :: XCMPLX_1:231

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