theorem :: XCMPLX_1:230

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