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