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