theorem :: XCMPLX_1:31

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