theorem :: XCMPLX_1:150

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