theorem Th73: :: ARYTM_3:73

for t being Element of RAT+ st t <> {} holds
ex r being Element of RAT+ st
( r < t & not r in omega )