theorem :: ARYTM_3:88

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