let j be Integer; :: thesis: ( j >= 1 or j = 0 or j < 0 )
( j < 0 or ( j is Element of NAT & ( j <> 0 or j = 0 ) ) ) by INT_1:3;
hence ( j >= 1 or j = 0 or j < 0 ) by NAT_1:14; :: thesis: verum