theorem :: NAT_D:48

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