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