:: deftheorem Def2 defines + XXREAL_3:def 2 :
for x, y, b₃ being ExtReal holds
( ( x is real & y is real implies ( b₃ = x + y iff ex a, b being Complex st
( x = a & y = b & b₃ = a + b ) ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ( b₃ = x + y iff b₃ = +infty ) ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( b₃ = x + y iff b₃ = -infty ) ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or ( b₃ = x + y iff b₃ = 0 ) ) );