theorem :: XCMPLX_1:228

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