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