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