theorem Th8: :: STIRL2_1:8

for n being Nat holds n is Subset of NAT