theorem Th46: :: NAT_D:46

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