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 A1: r <> s by Th69;
r <=' s by Def13;
hence r < s by A1, Th73; :: thesis: verum