theorem :: ARYTM_3:69

for r, s, t being Element of RAT+ st ( ( r < s & s <=' t ) or ( r <=' s & s < t ) ) holds
r < t by Th67;