theorem Th4: :: NAT_5:4

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