theorem :: XCMPLX_1:143

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