let x be Complex; :: thesis: x - 0 = x
x - 0 = x + 0 by Lm1, XCMPLX_0:def 8;
hence x - 0 = x by Th1; :: thesis: verum