theorem Th9: :: NAT_2:9

for i, j being non zero Nat holds i -' j < i