theorem Th1: :: NUMBER10:1

for i, j being natural Number st i < j holds
ex k being positive Nat st j = i + k