theorem :: ARYTM_2:17

for A being Subset of REAL+ st 0 in A & ( for x, y being Element of REAL+ st x in A & y = one holds
x + y in A ) holds
omega c= A