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 Th50;
then A1: r <> s by Th62;
r <=' s ;
hence r < s by A1, Th66; :: thesis: verum