let x be ExtReal; :: thesis: ( x <> +infty implies ( +infty - x = +infty & x - +infty = -infty ) )
assume A1: x <> +infty ; :: thesis: ( +infty - x = +infty & x - +infty = -infty )
then - x <> -infty by Th5;
hence +infty - x = +infty by Def2; :: thesis: x - +infty = -infty
- +infty = -infty by Def3;
hence x - +infty = -infty by A1, Def2; :: thesis: verum