theorem :: ARYTM_3:89

for r, s, t being Element of RAT+ st r <=' s & s <=' t & s <> t holds
r <> t by Th66;