let x, y, z be ExtReal; :: thesis: ( 0 <= x & 0 <= z & z + x < y implies z < y - x )
assume that
A1: 0 <= x and
A2: 0 <= z and
A3: z + x < y ; :: thesis: z < y - x
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 ( z <= y - x & z <> y - x ) by A3, Th22, Th45;
hence z < y - x by XXREAL_0:1; :: thesis: verum