( x = -infty & y = -infty ) by Theorem2;
hence not x + y is real by Def3; :: thesis: verum