thus - (+infty + -infty) = +infty - +infty by Def3
.= (- -infty) - +infty by Def3 ; :: thesis: verum