theorem Th5A: :: BAGORD_2:4

for m, n, x, y being Nat st x <= m & n = (m -' x) + y holds
x -' (m -' n) = y -' (n -' m)