for r, s, t being Element of RAT+ holds
( s + t <=' r + t iff s <=' r )