let
k
,
n
be
Nat
;
:: thesis:
(
k
<
n
implies
n
\/
{
k
}
=
n
)
assume
k
<
n
;
:: thesis:
n
\/
{
k
}
=
n
then
k
in
Segm
n
by
NAT_1:44
;
then
{
k
}
c=
n
by
ZFMISC_1:31
;
hence
n
\/
{
k
}
=
n
by
XBOOLE_1:12
;
:: thesis:
verum