let j be Integer; :: thesis: ( j >= 0 or j = - 1 or j < - 1 )

per cases ( j >= 0 or j < 0 ) ;

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

hence ( j >= 0 or j = - 1 or j < - 1 ) ; :: thesis: verum

end;

suppose A1: j < 0 ; :: thesis: ( j >= 0 or j = - 1 or j < - 1 )

then reconsider n = - j as Element of NAT by INT_1:3;
n <> - 0 by A1;
then n >= 1 by NAT_1:14;
then ( n > 1 or n = 1 ) by XXREAL_0:1;
then ( - 1 > - (- j) or - 1 = j ) by XREAL_1:24;
hence ( j >= 0 or j = - 1 or j < - 1 ) ; :: thesis: verum

end;

end;