let
n
be
Nat
;
:: thesis:
for
x
being
object
st
n
=
{
x
}
holds
x
=
0
let
x
be
object
;
:: thesis:
(
n
=
{
x
}
implies
x
=
0
)
assume
A1
:
n
=
{
x
}
;
:: thesis:
x
=
0
then
card
n
=
1
by
CARD_1:30
;
then
x
in
{
0
}
by
A1
,
CARD_1:49
,
TARSKI:def 1
;
hence
x
=
0
by
TARSKI:def 1
;
:: thesis:
verum