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 Th66;
take r ; :: thesis: ( r < t & not r in omega )
( r <=' one & r <> 1 ) by A2, A4, Def13, Th64;
then r < one by Th73;
hence r < t by A3, Th74; :: 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, Th46;
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 Th66;
A10: {} <=' r by Th71;
r <> {} by A1, A9, Th56;
then A11: {} < r by A10, Th73;
take r ; :: thesis: ( r < t & not r in omega )
A12: 1 = {} + one by Th56;
A13: 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 A13, Th73; :: thesis: not r in omega
r < one by A8, A13, Th74;
hence not r in omega by A11, A12, Th79; :: thesis: verum

end;

end;