let x, y, z be ExtReal; :: thesis: ( z is real implies (z + x) - (z + y) = x - y )
assume A1: z is real ; :: thesis: (z + x) - (z + y) = x - y

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

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

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

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

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

end;

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

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

end;

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

then consider a, b being Complex such that
A6: ( z = a & y = b ) and
z + y = a + b by A1, Def2;
reconsider a = a, b = b as Real by A1, A5, A6;
A7: a + b in REAL by XREAL_0:def 1;
(z + -infty) - (z + y) = -infty - (z + y) by A1, Def2
.= -infty by A6, A7, Def2
.= -infty - y by A5, Def2 ;
hence (z + x) - (z + y) = x - y by A2; :: thesis: verum

end;

end;

end;

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

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

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

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

end;

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

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

end;

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

then consider a, b being Complex such that
A12: ( z = a & x = b ) and
z + x = a + b by A1, Def2;
reconsider a = a, b = b as Real by A1, A11, A12;
A13: a + b in REAL by XREAL_0:def 1;
A14: - +infty = -infty by Def3;
(z + x) - (z + +infty) = (z + x) - +infty by A1, Def2
.= (z + x) + -infty by Def3
.= -infty by A12, A13, Def2
.= x + (- +infty) by A11, A14, Def2 ;
hence (z + x) - (z + y) = x - y by A8; :: thesis: verum

end;

end;

end;

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

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

end;

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

then reconsider c = z, b = y as Real ;
A16: z + y = c + b ;
( z + x = +infty & x - y = +infty ) by A15, Def2;
hence (z + x) - (z + y) = x - y by A16, Th13; :: thesis: verum

end;

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

then reconsider c = z, a = x as Real ;
( z + x = c + a & z + y = -infty ) by A17, Def2;
then (z + x) - (z + y) = +infty by Th14
.= x - y by A17, Th14 ;
hence (z + x) - (z + y) = x - y ; :: thesis: verum

end;

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

then ( z + y = -infty & not z + x = -infty ) by Def2;
then (z + x) - (z + y) = +infty by Th14
.= x - y by A18, Th14 ;
hence (z + x) - (z + y) = x - y ; :: thesis: verum

end;

end;