( x = -infty & y = +infty ) by Th1, Th2;
hence x + y is zero by Def2; :: thesis: verum