let x, z be ExtReal; :: thesis: ( 0 <= z implies x <= x + z )
assume 0 <= z ; :: thesis: x <= x + z
then x + 0 <= x + z by Th36;
hence x <= x + z by Th4; :: thesis: verum