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

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) = (- x) + (- y)

hence - (x + y) = - +infty by Def2
.= (- x) + (- y) by A1, Def2, Lm5 ;
:: thesis: verum

end;

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

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

end;

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

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

end;

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

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

end;

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

hence - (x + y) = - -infty by Def2
.= (- x) + (- y) by A2, Def2, Th5 ;
:: thesis: verum

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;