Description: The set of positive integers is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021)