for x, y, z being ExtReal st z in REAL & x < y holds
( x + z < y + z & x - z < y - z )