let x be complex number ; :: according to MEMBERED:def 25 :: thesis: for y being complex number st x in COMPLEX & y in COMPLEX holds
x + y in COMPLEX
thus for y being complex number st x in COMPLEX & y in COMPLEX holds
x + y in COMPLEX by XCMPLX_0:def 2; :: thesis: verum