let x, y be R_eal; :: thesis: - (x + y) = (- y) - x

per cases ( ( x = +infty & y = +infty ) or ( x = +infty & y = -infty ) or ( x = +infty & y in REAL ) or ( x = -infty & y = +infty ) or ( x = -infty & y = -infty ) or ( x = -infty & y in REAL ) or ( x in REAL & y = +infty ) or ( x in REAL & y = -infty ) or ( x in REAL & y in REAL ) ) by XXREAL_0:14;

suppose A1: ( x = +infty & y = +infty ) ; :: thesis: - (x + y) = (- y) - x

hence - (x + y) = - +infty by SUPINF_2:def 2
.= (- y) - x by A1, Lm3, SUPINF_2:def 2 ;
:: thesis: verum

end;

suppose ( x = +infty & y = -infty ) ; :: thesis: - (x + y) = (- y) - x

hence - (x + y) = (- y) - x by Lm4; :: thesis: verum

end;

suppose ( x = +infty & y in REAL ) ; :: thesis: - (x + y) = (- y) - x

hence - (x + y) = (- y) - x by Lm5; :: thesis: verum

end;

suppose ( x = -infty & y = +infty ) ; :: thesis: - (x + y) = (- y) - x

hence - (x + y) = (- y) - x by Lm4; :: thesis: verum

end;

suppose A2: ( x = -infty & y = -infty ) ; :: thesis: - (x + y) = (- y) - x

hence - (x + y) = - -infty by SUPINF_2:def 2
.= (- y) - x by A2, SUPINF_2:4, SUPINF_2:def 2 ;
:: thesis: verum

end;

suppose ( x = -infty & y in REAL ) ; :: thesis: - (x + y) = (- y) - x

hence - (x + y) = (- y) - x by Lm6; :: thesis: verum

end;

suppose ( x in REAL & y = +infty ) ; :: thesis: - (x + y) = (- y) - x

hence - (x + y) = (- y) - x by Lm5; :: thesis: verum

end;

suppose ( x in REAL & y = -infty ) ; :: thesis: - (x + y) = (- y) - x

hence - (x + y) = (- y) - x by Lm6; :: thesis: verum

end;

suppose ( x in REAL & y in REAL ) ; :: thesis: - (x + y) = (- y) - x

then reconsider a = x, b = y as Real ;
A3: ( x + y = a + b & - x = - a & - y = - b ) by SUPINF_2:1, SUPINF_2:3;
then - (x + y) = - (a + b) by SUPINF_2:3
.= (- a) + (- b) ;
hence - (x + y) = (- y) - x by A3, SUPINF_2:1; :: thesis: verum

end;

end;