for n being Nat holds n is Subset of NAT