let x, y, z be ExtReal; :: thesis: ( 0 <= x & 0 <= z & z + x < y implies z <= y )
assume that
A1: 0 <= x and
A2: 0 <= z and
A3: z + x < y ; :: thesis: z <= y
x in REAL

proof

A4: x <> +infty

proof

assume x = +infty ; :: thesis: contradiction
then +infty < y by A2, A3, Def2;
hence contradiction by XXREAL_0:4; :: thesis: verum

end;

assume not x in REAL ; :: thesis: contradiction
hence contradiction by A1, A4, XXREAL_0:10, Lm16; :: thesis: verum

end;

then A5: (z + x) - x = z by Th22;
y - 0 = y by Th15;
hence z <= y by A1, A3, A5, Th37; :: thesis: verum