:: deftheorem Def6 defines + ARYTM_2:def 6 :
for A, B being Element of DEDEKIND_CUTS holds A + B = { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } ;