let i1 be Integer; :: thesis: ( i1 < 0 implies i1 <= - 1 )
assume i1 < 0 ; :: thesis: i1 <= - 1
then 0 < - i1 by XREAL_1:58;
then 1 <= - i1 by Lm4;
then - (- i1) <= - 1 by XREAL_1:24;
hence i1 <= - 1 ; :: thesis: verum