let x be ext-real number ; :: 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 Tx4A;
hence +infty - x = +infty by Def3; :: thesis: x - +infty = -infty
- +infty = -infty by Def5;
hence x - +infty = -infty by A1, Def3; :: thesis: verum