let x, y be ExtReal; :: 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 Def2
.= (- y) - x by A1, Def2, Lm10 ;
:: 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 Lm6; :: 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 Def2
.= (- y) - x by A2, Def2, Th5 ;
:: thesis: verum

end;

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

hence - (x + y) = (- y) - x by Lm11; :: 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 = -infty ) ; :: thesis: - (x + y) = (- y) - x

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

end;

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

then reconsider a = x, b = y as Real ;
- (x + y) = - (a + b)
.= (- a) + (- b) ;
hence - (x + y) = (- y) - x ; :: thesis: verum

end;

end;