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
x is Real

proof

assume A3: x is not Real ; :: thesis: contradiction
A4: ( x in REAL or x in {-infty ,+infty } ) by XBOOLE_0:def 3, XXREAL_0:def 4;
x <> +infty

proof

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

end;

hence contradiction by A1, A3, A4, SUPINF_2:19, TARSKI:def 2; :: thesis: verum

end;

then ( (z + x) - x = z & y - 0. = y ) by Th8, Th21;
hence z <= y by A1, SUPINF_2:15; :: thesis: verum