for x, y, z being Element of REAL+ holds
( x <=' y iff x + z <=' y + z )