theorem :: ARYTM_1:14

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