let x be R_eal; :: thesis: ( x <> +infty & x <> -infty implies ex y being R_eal st x + y = 0 )
assume ( x <> +infty & x <> -infty ) ; :: thesis: ex y being R_eal st x + y = 0
then reconsider a = x as Real by XXREAL_0:14;
reconsider b = - a as Real ;
A1: a + b = 0 ;
A2: R_EAL b = b by MEASURE6:def 1;
take R_EAL b ; :: thesis: x + (R_EAL b) = 0
thus x + (R_EAL b) = 0 by A1, A2, SUPINF_2:1; :: thesis: verum