theorem :: XCMPLX_1:38

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