theorem Th13: :: XXREAL_3:13

for x being ExtReal st x <> +infty holds
( +infty - x = +infty & x - +infty = -infty )