let
n
,
m
,
l
be
Nat
;
:: thesis:
{
n
,
m
,
l
}
is
finite
Subset
of
NAT
reconsider
Y
=
{
m
,
l
}
as
finite
Subset
of
NAT
by
Th5
;
reconsider
X
=
{
n
}
as
finite
Subset
of
NAT
by
Th4
;
{
n
,
m
,
l
}
=
X
\/
Y
by
ENUMSET1:2
;
hence
{
n
,
m
,
l
}
is
finite
Subset
of
NAT
;
:: thesis:
verum