let i1 be Integer; :: thesis: ( i1 < 0 implies i1 <= - 1 )
assume i1 < 0 ; :: thesis: i1 <= - 1
then 0 < - i1 by XREAL_1:60;
then 1 <= - i1 by Lm5;
then - (- i1) <= - 1 by XREAL_1:26;
hence i1 <= - 1 ; :: thesis: verum