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 that
A1: i < x and
A2: x < i + one and
A3: x in omega ; :: thesis: contradiction
consider z being Element of RAT+ such that
A4: i + one = x + z by A2, Def13;
i + one = i +^ 1 by Th58;
then i + one in omega by Th31;
then reconsider z9 = z as Element of omega by A3, A4, Th71;
consider y being Element of RAT+ such that
A5: x = i + y by A1, Def13;
i in omega by Th31;
then reconsider y9 = y as Element of omega by A3, A5, Th71;
i + one = i + (y + z) by A5, A4, Th51;
then 1 = y + z by Th62
.= y9 +^ z9 by Th58 ;
then y9 c= 1 by ORDINAL3:24;
then ( y = {} or y = 1 ) by ORDINAL3:16;
then ( i = x or i + one = x ) by A5, Th50;
hence contradiction by A1, A2; :: thesis: verum