:: deftheorem Def1 defines + ARYTM_0:def 1 :
for x, y, b₃ being Element of REAL holds
( ( x in REAL+ & y in REAL+ implies ( b₃ = + (x,y) iff ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & b₃ = x9 + y9 ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] implies ( b₃ = + (x,y) iff ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & b₃ = x9 - y9 ) ) ) & ( y in REAL+ & x in [:{0},REAL+:] implies ( b₃ = + (x,y) iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b₃ = y9 - x9 ) ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) implies ( b₃ = + (x,y) iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b₃ = [0,(x9 + y9)] ) ) ) );