x = +infty by Th1;
hence not x + y is real by Def2; :: thesis: verum