theorem :: XCMPLX_1:121

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