let r be Element of RAT+ ; :: thesis: ex s being Element of RAT+ st r < s
take s = r + one ; :: thesis: r < s
s + {} = s by Th56;
then ( r <=' s & r <> s ) by Def13, Th69;
hence r < s by Th73; :: thesis: verum