theorem Th13: :: NAT_1:13

for i, j being natural Number holds
( i < j + 1 iff i <= j )