theorem :: ARYTM_1:23

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