theorem :: ARYTM_2:16

for x, y being Element of REAL+ st x in omega & y in omega holds
y + x in omega