theorem :: XCMPLX_1:68
for a being Complex holds ((a / 3) + (a / 3)) + (a / 3) = a ;