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