let x be R_eal; :: thesis: ( ( x = +infty or x = -infty ) implies for y being R_eal st y in REAL holds
x + y <> 0 )
assume A1: ( x = +infty or x = -infty ) ; :: thesis: for y being R_eal st y in REAL holds
x + y <> 0
given y being R_eal such that A2: ( y in REAL & x + y = 0 ) ; :: thesis: contradiction

per cases ( x = +infty or x = -infty ) by A1;

suppose x = +infty ; :: thesis: contradiction

hence contradiction by A2, SUPINF_2:def 2; :: thesis: verum

end;

suppose x = -infty ; :: thesis: contradiction

hence contradiction by A2, SUPINF_2:def 2; :: thesis: verum

end;

end;