theorem :: XCMPLX_1:157

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