let
a
be
Nat
;
:: thesis:
seq
(
a
,
0
)
=
{}
hereby
:: thesis:
verum
set
x
= the
Element
of
seq
(
a
,
0
);
assume
A1
:
seq
(
a
,
0
)
<>
{}
;
:: thesis:
contradiction
then
reconsider
x
= the
Element
of
seq
(
a
,
0
) as
Element
of
NAT
by
TARSKI:def 3
;
( 1
+
a
<=
x
&
x
<=
0
+
a
)
by
A1
,
Th1
;
hence
contradiction
by
NAT_1:13
;
:: thesis:
verum
end;