theorem :: ARYTM_3:87

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