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