let n be natural number ; :: thesis: {n} is finite Subset of NAT
n in NAT by ORDINAL1:def 13;
hence {n} is finite Subset of NAT by ZFMISC_1:37; :: thesis: verum