theorem :: NAT_D:49

for i1, i2 being natural Number st ( i1 < i2 or i1 + 1 <= i2 ) holds
i1 <= i2 -' 1