theorem :: XCMPLX_1:18

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