theorem :: ARYTM_3:77

for s, t being Element of RAT+ holds s <=' s + t ;