0 + (- 0) = - 0 by Th1;
hence - 0 = 0 by XCMPLX_0:def 6; :: thesis: verum