theorem Th8: :: INT_1:8

for i1 being Integer st i1 < 0 holds
i1 <= - 1