theorem :: XCMPLX_1:194

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