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

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

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

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

end;

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

then y - x = -infty by Def2;
hence ( (y - x) + x = y & (y + x) - x = y ) by A3, Def2; :: thesis: verum

end;

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

then y - x = +infty by Def2;
hence ( (y - x) + x = y & (y + x) - x = y ) by A4, Def2; :: thesis: verum

end;

end;