let x, z, y be ext-real number ; :: 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 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 A5: z <= y - x by A1, MEA2;
z <> y - x by A1, A2, Th44;
hence z < y - x by A5, XXREAL_0:1; :: thesis: verum