let x, z, y be ext-real number ; :: thesis: ( 0 <= x & z + x <= y implies z <= y )
assume 0 <= x ; :: thesis: ( not z + x <= y or z <= y )
then A1: z <= z + x by Th28;
assume z + x <= y ; :: thesis: z <= y
hence z <= y by A1, XXREAL_0:2; :: thesis: verum