theorem :: XCMPLX_1:29

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