let x, y, z be R_eal; :: thesis: ( 0. <= x & 0. <= z & z + x < y implies z < y - x )
assume A1: ( 0. <= x & 0. <= z & z + x < y ) ; :: thesis: z < y - x
A2: 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 A5: z <= y - x by A1, MEASURE4:2;
z <> y - x by A1, A2, Th8;
hence z < y - x by A5, XXREAL_0:1; :: thesis: verum