theorem Th72: :: ARYTM_3:72

for x being Element of RAT+
for i being ordinal Element of RAT+ st i < x & x < i + one holds
not x in omega