let x be ordinal Element of RAT+ ; :: thesis: x is natural
assume not x in omega ; :: according to ORDINAL1:def 12 :: thesis: contradiction
then A1: ex i, j being Element of omega st
( x = [i,j] & i,j are_coprime & j <> {} & j <> 1 ) by Th29;
then {} in x by ORDINAL3:8;
hence contradiction by A1, TARSKI:def 2; :: thesis: verum