theorem Th5: :: INT_1:5

for i1, i2 being Integer st i2 <= i1 holds
i1 - i2 in NAT