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