let t be Element of RAT+ ; :: thesis: ( t <> {} implies ex r being Element of RAT+ st
( r < t & not r in omega ) )
assume A1: t <> {} ; :: thesis: ex r being Element of RAT+ st
( r < t & not r in omega )
A2: 1 +^ 1 = succ 1 by ORDINAL2:48;

per cases ( one <=' t or t < one ) ;

suppose A3: one <=' t ; :: thesis: ex r being Element of RAT+ st
( r < t & not r in omega )

consider r being Element of RAT+ such that
A4: one = r + r by Th66;
take r ; :: thesis: ( r < t & not r in omega )
A5: r <=' one by A4, Def13;
r <> 1 by A2, A4, Th64;
then r < one by A5, Th73;
hence r < t by A3, Th74; :: thesis: not r in omega
assume r in omega ; :: thesis: contradiction
then A6: ( denominator r = 1 & denominator one = 1 ) by Def9;
then ( (numerator r) *^ (denominator r) = numerator r & 1 *^ 1 = 1 ) by ORDINAL2:56;
then A7: 1 = (numerator r) +^ (numerator r) by A4, A6, Th46;
then numerator r c= 1 by ORDINAL3:27;
then ( numerator r = {} or numerator r = 1 ) by ORDINAL3:19;
hence contradiction by A2, A7, ORDINAL2:44; :: thesis: verum

end;

suppose A8: t < one ; :: thesis: ex r being Element of RAT+ st
( r < t & not r in omega )

consider r being Element of RAT+ such that
A9: t = r + r by Th66;
take r ; :: thesis: ( r < t & not r in omega )
A10: r <=' t by A9, Def13;

now

assume r = t ; :: thesis: contradiction
then t + {} = t + t by A9, Th56;
hence contradiction by A1, Th69; :: thesis: verum

end;

hence r < t by A10, Th73; :: thesis: not r in omega
A11: r < one by A8, A10, Th74;
( r <> {} & {} <=' r ) by A1, A9, Th56, Th71;
then ( {} < r & 1 = {} + one ) by Th56, Th73;
hence not r in omega by A11, Th79; :: thesis: verum

end;

end;