theorem :: XCMPLX_1:180

for a being Complex holds (- a) * (- 1) = a ;