theorem Th89: :: ORDINAL7:76

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