let A be Ordinal; :: thesis: ( A in RAT+ implies A in omega )
assume ( A in RAT+ & not A in omega ) ; :: thesis: contradiction
then ex i, j being Element of omega st
( A = [i,j] & i,j are_coprime & j <> {} & j <> 1 ) by Th29;
hence contradiction by Th30; :: thesis: verum