theorem :: ARYTM_1:12

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