theorem :: XCMPLX_1:21

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