let x, y be ext-real number ; :: 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 Def3
.= (- y) - x by A1, Lm3, Def3 ;
:: 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 Def3
.= (- y) - x by A2, Tx4A, Def3 ;
:: 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 number ;
- (x + y) = - (a + b)
.= (- a) + (- b) ;
hence - (x + y) = (- y) - x ; :: thesis: verum

end;

end;