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