theorem :: XXREAL_3:53

for x, y, z being ExtReal holds
( ( z = +infty & y = +infty ) or ( z = -infty & y = -infty ) or not x < z - y or ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) )