let x be ordinal Element of RAT+ ; :: thesis: x is natural
assume not x in omega ; :: according to ORDINAL1:def 13 :: thesis: contradiction
then consider i, j being Element of omega such that
A1: ( x = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 ) by Th35;
{} in x by A1, ORDINAL3:10;
hence contradiction by A1, TARSKI:def 2; :: thesis: verum