theorem :: ARYTM_3:94

for r being Element of RAT+ ex s being Element of RAT+ st r < s