theorem :: XCMPLX_1:144

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