theorem :: XCMPLX_1:193

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