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:31;

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 Th60;
take r ; :: thesis: ( r < t & not r in omega )
( r <=' one & r <> 1 ) by A2, A4, Th58;
then r < one by Th66;
hence r < t by A3, Th67; :: thesis: not r in omega
A5: 1 *^ 1 = 1 by ORDINAL2:39;
assume r in omega ; :: thesis: contradiction
then A6: denominator r = 1 by Def9;
then (numerator r) *^ (denominator r) = numerator r by ORDINAL2:39;
then A7: 1 = (numerator r) +^ (numerator r) by A4, A6, A5, Th40;
then numerator r c= 1 by ORDINAL3:24;
then ( numerator r = {} or numerator r = 1 ) by ORDINAL3:16;
hence contradiction by A2, A7, ORDINAL2:27; :: 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 Th60;
A10: {} <=' r by Th64;
r <> {} by A1, A9, Th50;
then A11: {} < r by A10, Th66;
take r ; :: thesis: ( r < t & not r in omega )
A12: 1 = {} + one by Th50;
A13: r <=' t by A9;

now :: thesis: not r = t

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

end;

hence r < t by A13, Th66; :: thesis: not r in omega
r < one by A8, A13, Th67;
hence not r in omega by A11, A12, Th72; :: thesis: verum

end;

end;