theorem Th10: :: NAT_1:10

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