let x be Element of RAT+ ; :: thesis: for i being ordinal Element of RAT+ st i < x & x < i + one holds
not x in omega
let i be ordinal Element of RAT+ ; :: thesis: ( i < x & x < i + one implies not x in omega )
assume A1: ( i < x & x < i + one & x in omega ) ; :: thesis: contradiction
then consider y being Element of RAT+ such that
A2: x = i + y by Def13;
consider z being Element of RAT+ such that
A3: i + one = x + z by A1, Def13;
i + one = i +^ 1 by Th64;
then i + one in omega by Th37;
then reconsider z' = z as Element of omega by A1, A3, Th78;
i in omega by Th37;
then reconsider y' = y as Element of omega by A1, A2, Th78;
i + one = i + (y + z) by A2, A3, Th57;
then 1 = y + z by Th69
.= y' +^ z' by Th64 ;
then ( y' c= 1 & z' c= 1 ) by ORDINAL3:27;
then ( ( y = {} or y = 1 ) & ( z = {} or z = 1 ) ) by ORDINAL3:19;
then ( i = x or i + one = x ) by A2, Th56;
hence contradiction by A1; :: thesis: verum