let
n
be
Nat
;
:: thesis:
min*
n
=
0
now
:: thesis:
min*
n
=
0
per
cases
(
0
=
n
or
0
<
n
)
;
suppose
0
=
n
;
:: thesis:
min*
n
=
0
hence
min*
n
=
0
by
NAT_1:def 1
;
:: thesis:
verum
end;
suppose
0
<
n
;
:: thesis:
min*
n
=
0
then
0
in
{
l
where
l
is
Nat
:
l
<
n
}
;
then
A1
:
0
in
n
by
AXIOMS:4
;
n
is
Subset
of
NAT
by
Th8
;
hence
min*
n
=
0
by
A1
,
NAT_1:def 1
;
:: thesis:
verum
end;
end;
end;
hence
min*
n
=
0
;
:: thesis:
verum