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

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

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

then x + z = +infty by A1, Def2;
hence x = (x + z) - z by A1, A2, Th13; :: thesis: verum

end;

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

then x + z = -infty by A1, Def2;
hence x = (x + z) - z by A1, A3, Th14; :: thesis: verum

end;

suppose x is Element of REAL ; :: thesis: x = (x + z) - z

then reconsider a = x, c = z as Real by A1;
(x + z) - z = (a + c) - c ;
hence x = (x + z) - z ; :: thesis: verum

end;

end;