let x, y be Element of REAL+ ; :: thesis: (x + y) -' y = x
y <=' x + y by ARYTM_2:19;
hence (x + y) -' y = x by Def1; :: thesis: verum