for r, s, t being Element of RAT+ st r <=' s & s <=' r + t holds
ex t0 being Element of RAT+ st
( s = r + t0 & t0 <=' t ) by Th76;