let x, y, z be R_eal; :: thesis: ( z in REAL & x <= y implies ( z + x <= z + y & x + z <= y + z & x - z <= y - z ) )
assume A1: ( z in REAL & x <= y ) ; :: thesis: ( z + x <= z + y & x + z <= y + z & x - z <= y - z )

per cases ( x = y or x <> y ) ;

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

hence ( z + x <= z + y & x + z <= y + z & x - z <= y - z ) ; :: thesis: verum

end;

suppose A2: x <> y ; :: thesis: ( z + x <= z + y & x + z <= y + z & x - z <= y - z )

A3: ( ( x in REAL or x in {-infty ,+infty } ) & ( y in REAL or y in {-infty ,+infty } ) ) by XBOOLE_0:def 3, XXREAL_0:def 4;
A4: ( not x in REAL or not y = -infty ) by A1, XXREAL_0:6;
A5: ( not x = -infty or not y = -infty ) by A2;
A6: ( not x = +infty or not y in REAL ) by A1, XXREAL_0:4;
A7: ( not x = +infty or not y = -infty ) by A1, XXREAL_0:7;
A8: ( not x = +infty or not y = +infty ) by A2;

now

per cases ( ( x in REAL & y in REAL ) or ( x in REAL & y = +infty ) or ( x = -infty & y in REAL ) or ( x = -infty & y = +infty ) ) by A3, A4, A5, A6, A7, A8, TARSKI:def 2;

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

then reconsider a = x, b = y, c = z as Real by A1;
reconsider w = x + z, r = y + z as R_eal ;
reconsider p = a + c, q = b + c as Real ;
A9: ( w = p & r = q ) by SUPINF_2:1;
reconsider w = x - z, r = y - z as R_eal ;
reconsider p = a - c, q = b - c as Real ;
( w = p & r = q ) by SUPINF_2:5;
hence ( z + x <= z + y & x + z <= y + z & x - z <= y - z ) by A1, A9, XREAL_1:8, XREAL_1:11; :: thesis: verum

end;

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

then ( z + y = +infty & y + z = +infty & y - z = +infty ) by A1, SUPINF_2:6, SUPINF_2:def 2;
hence ( z + x <= z + y & x + z <= y + z & x - z <= y - z ) by XXREAL_0:4; :: thesis: verum

end;

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

then ( z + x = -infty & x + z = -infty & x - z = -infty ) by A1, SUPINF_2:7, SUPINF_2:def 2;
hence ( z + x <= z + y & x + z <= y + z & x - z <= y - z ) by XXREAL_0:5; :: thesis: verum

end;

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

then ( z + x = -infty & z + y = +infty & x + z = -infty & y + z = +infty & x - z = -infty & y - z = +infty ) by A1, SUPINF_2:6, SUPINF_2:7, SUPINF_2:def 2;
hence ( z + x <= z + y & x + z <= y + z & x - z <= y - z ) by XXREAL_0:4; :: thesis: verum

end;

end;

end;

hence ( z + x <= z + y & x + z <= y + z & x - z <= y - z ) ; :: thesis: verum

end;

end;