theorem Th42: :: NAT_D:42

for n, i1, i2 being natural Number st i1 <= i2 holds
i1 -' n <= i2 -' n