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