theorem :: XCMPLX_1:163

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