theorem :: XCMPLX_1:32

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