:: deftheorem Def8 defines + ARYTM_2:def 8 :
for x, y being Element of REAL+ holds
( ( y = {} implies x + y = x ) & ( x = {} implies x + y = y ) & ( not y = {} & not x = {} implies x + y = GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) ) );