let z, x be ext-real number ; :: 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 Tx3; :: thesis: verum