theorem :: XCMPLX_1:22

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