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