theorem :: XCMPLX_1:37

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