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