:: deftheorem Def13 defines <=' ARYTM_3:def 13 :
for x, y being Element of RAT+ holds
( x <=' y iff ex z being Element of RAT+ st y = x + z );