let r1, r2, s1, s2 be Element of RAT+ ; :: thesis: ( not r1 + r2 = s1 + s2 or r1 <=' s1 or r2 <=' s2 )
assume A1: r1 + r2 = s1 + s2 ; :: thesis: ( r1 <=' s1 or r2 <=' s2 )
assume that
A2: s1 < r1 and
A3: s2 < r2 ; :: thesis: contradiction
s1 + s2 < r1 + s2 by A2, Th76;
hence contradiction by A1, A3, Th76; :: thesis: verum