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

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

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;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