let
x
be non
zero
Nat
;
:: thesis:
0
in
x
reconsider
n
=
x
as
Element
of
NAT
by
ORDINAL1:def 12
;
(
n
=
{
i
where
i
is
Nat
:
i
<
n
}
&
0
<
n
)
by
AXIOMS:4
;
hence
0
in
x
;
:: thesis:
verum