let i be Integer; :: thesis: ( i >= - 1 & i <= 0 & not i = - 1 implies i = 0 )
assume that
A1: i >= - 1 and
A2: i <= 0 ; :: thesis: ( i = - 1 or i = 0 )

per cases ( i <= - 1 or i > - 1 ) ;

suppose i <= - 1 ; :: thesis: ( i = - 1 or i = 0 )

hence ( i = - 1 or i = 0 ) by A1, XXREAL_0:1; :: thesis: verum

end;

suppose i > - 1 ; :: thesis: ( i = - 1 or i = 0 )

then i >= (- 1) + 1 by INT_1:7;
hence ( i = - 1 or i = 0 ) by A2; :: thesis: verum

end;

end;