theorem Th13: :: ARYTM_1:13

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