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