theorem :: ARYTM_3:74

for t being Element of RAT+ holds
( { s where s is Element of RAT+ : s < t } in RAT+ iff t = {} )