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