theorem :: NAT_1:9

for i, j being natural Number st i <= j & j <= i + 1 & not i = j holds
j = i + 1