let x, y, z be ExtReal; :: thesis: ( 0 <= x & z + x <= y implies z <= y )
assume 0 <= x ; :: thesis: ( not z + x <= y or z <= y )
then z <= z + x by Th39;
hence ( not z + x <= y or z <= y ) by XXREAL_0:2; :: thesis: verum