not y in REAL ;
then A1: ( y = -infty or y = +infty ) by XXREAL_0:14;
let z be object ; :: thesis: ( z = x + y implies not z is real )
assume z = x + y ; :: thesis: not z is real
hence not z is real by A1, Def2; :: thesis: verum