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 )

now :: thesis: not - x = +infty

assume - x = +infty ; :: thesis: contradiction
then - (- x) = -infty by Def3;
hence contradiction by A1; :: thesis: verum

end;

hence -infty - x = -infty by Def2; :: thesis: x - -infty = +infty
thus x - -infty = +infty by A1, Def2, Th5; :: thesis: verum