let
S
be
Subset
of
NAT
;
:: thesis:
(
S
=
SegM
n
iff
S
=
{
k
where
k
is
Nat
:
k
<=
n
}
)
SegM
(
Segm
n
)
=
{
k
where
k
is
Nat
:
k
<=
n
}
by
NAT_1:54
;
hence
(
S
=
SegM
n
iff
S
=
{
k
where
k
is
Nat
:
k
<=
n
}
) ;
:: thesis:
verum