let x be ExtReal; :: thesis: ( x in REAL implies - (x + -infty) = (- -infty) + (- x) )
A1: - -infty = +infty by Th23;
assume A2: x in REAL ; :: thesis: - (x + -infty) = (- -infty) + (- x)
then x + -infty = -infty by Def2;
hence - (x + -infty) = (- -infty) + (- x) by A2, A1, Def2; :: thesis: verum