for x, y being Real st x in NAT & y in NAT holds
x + y in NAT