theorem :: XCMPLX_1:148

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