theorem Th71: :: ARYTM_3:71

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