let x be ext-real number ; :: thesis: ( x in REAL implies - (x + +infty ) = (- +infty ) + (- x) )
assume A1: x in REAL ; :: thesis: - (x + +infty ) = (- +infty ) + (- x)
x + +infty = +infty by A1, Def3;
hence - (x + +infty ) = (- +infty ) + (- x) by Tx4B, A1, Def3; :: thesis: verum