for n being Nat holds {n} is finite Subset of NAT by ORDINAL1:def 12, ZFMISC_1:31;