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

proof

assume A3: not x in REAL ; :: thesis: contradiction
x <> +infty

proof

assume x = +infty ; :: thesis: contradiction
then +infty < y by A1, Def3;
hence contradiction by XXREAL_0:4; :: thesis: verum

end;

hence contradiction by A1, A3, XXREAL_0:10; :: thesis: verum

end;

then ( (z + x) - x = z & y - 0 = y ) by Th44, Th21;
hence z <= y by A1, Th37; :: thesis: verum