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

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

suppose A2: x in REAL ; :: thesis: z <= y

( (z + x) - x = z & y - 0. = y ) by A2, MEASURE6:8, MEASURE6:21;
hence z <= y by A1, SUPINF_2:15; :: thesis: verum

end;

suppose x = +infty ; :: thesis: z <= y

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

end;

end;