let s1, t1, s2, t2 be Element of RAT+ ; :: thesis: ( s1 + t1 = s2 + t2 & s1 <=' s2 implies t2 <=' t1 )
assume A1: s1 + t1 = s2 + t2 ; :: thesis: ( not s1 <=' s2 or t2 <=' t1 )
given x being Element of RAT+ such that A2: s2 = s1 + x ; :: according to ARYTM_3:def 13 :: thesis: t2 <=' t1
take x ; :: according to ARYTM_3:def 13 :: thesis: t1 = t2 + x
s1 + t1 = s1 + (x + t2) by A1, A2, Th51;
hence t1 = t2 + x by Th62; :: thesis: verum