theorem Th6: :: BAGORD_2:1

for m, n being Nat holds n = (m -' (m -' n)) + (n -' m)