let
n
be
Element
of
NAT
;
:: thesis:
(
min*
{
n
}
=
n
&
min
{
n
}
=
n
)
A1
:
min*
{
n
}
in
{
n
}
by
NAT_1:def 1
;
min*
{
n
}
=
min
{
n
}
by
Th1
;
hence
(
min*
{
n
}
=
n
&
min
{
n
}
=
n
)
by
A1
,
TARSKI:def 1
;
:: thesis:
verum