let z, z1 be Complex; :: thesis: [z1,(z1 + z)] in addRel (COMPLEX,z)
( z1 in COMPLEX & z1 + z in COMPLEX ) by XCMPLX_0:def 2;
hence [z1,(z1 + z)] in addRel (COMPLEX,z) by Th11; :: thesis: verum