theorem :: XCMPLX_1:39

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