let z, x, y be ext-real number ; :: 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 S: 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 SS: y = -infty ; :: thesis: (z + x) - (z + y) = x - y

(z + -infty ) - (z + -infty ) = -infty - (z + -infty ) by A1, Def3
.= -infty - -infty by A1, Def3 ;
hence (z + x) - (z + y) = x - y by S, SS; :: thesis: verum

end;

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

(z + -infty ) - (z + +infty ) = -infty - (z + +infty ) by A1, Def3
.= -infty - +infty by A1, Def3 ;
hence (z + x) - (z + y) = x - y by S, SS; :: thesis: verum

end;

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

then consider a, b being complex number such that
TT: ( z = a & y = b & z + y = a + b ) by A1, Def3;
reconsider a = a, b = b as real number by A1, SS, TT;
YY: a + b in REAL by XREAL_0:def 1;
(z + -infty ) - (z + y) = -infty - (z + y) by A1, Def3
.= -infty by YY, Def3, TT
.= -infty - y by SS, Def3 ;
hence (z + x) - (z + y) = x - y by S; :: thesis: verum

end;

end;

end;

suppose S: 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 SS: x = -infty ; :: thesis: (z + x) - (z + y) = x - y

(z + -infty ) - (z + +infty ) = (z + -infty ) - +infty by A1, Def3
.= -infty - +infty by A1, Def3 ;
hence (z + x) - (z + y) = x - y by S, SS; :: thesis: verum

end;

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

(z + +infty ) - (z + +infty ) = (z + +infty ) - +infty by A1, Def3
.= +infty - +infty by A1, Def3 ;
hence (z + x) - (z + y) = x - y by S, SS; :: thesis: verum

end;

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

then consider a, b being complex number such that
TT: ( z = a & x = b & z + x = a + b ) by A1, Def3;
A: - +infty = -infty by Def5;
reconsider a = a, b = b as real number by A1, SS, TT;
VV: a + b in REAL by XREAL_0:def 1;
(z + x) - (z + +infty ) = (z + x) - +infty by A1, Def3
.= (z + x) + -infty by Def5
.= -infty by VV, TT, Def3
.= x + (- +infty ) by SS, A, Def3 ;
hence (z + x) - (z + y) = x - y by S; :: 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 number ;
(z + x) - (z + y) = (a + c) - (c + b)
.= a - b
.= x - y ;
hence (z + x) - (z + y) = x - y ; :: thesis: verum

end;

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

then reconsider c = z, b = y as real number ;
A5: z + y = c + b ;
( z + x = +infty & x - y = +infty ) by A4, Def3;
hence (z + x) - (z + y) = x - y by A5, Th16; :: thesis: verum

end;

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

then reconsider c = z, a = x as real number ;
A7: z + x = c + a ;
z + y = -infty by A6, Def3;
then (z + x) - (z + y) = +infty by A7, Th29
.= x - y by A6, Th29 ;
hence (z + x) - (z + y) = x - y ; :: thesis: verum

end;

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

then ( z + y = -infty & not z + x = -infty ) by Def3;
then (z + x) - (z + y) = +infty by Th29
.= x - y by A8, Th29 ;
hence (z + x) - (z + y) = x - y ; :: thesis: verum

end;

end;