Description: Positive integers are a subset of integers. (Contributed by NM, 9-Jan-2002)
|- NN C_ ZZ
|- ( x e. NN -> x e. ZZ )