Let $\mathbb{N}$ be the set of \reftext{def:natural-numbers-2026a}{natural numbers} with successor map $S$, let $\le$ be the \reftext{def:order-natural-numbers-2026a}{order} on $\mathbb{N}$, let $[n]$ denote the \reftext{def:initial-segment-natural-numbers-2026a}{initial segment} determined by $n$, and let the notions \reftext{def:number-of-elements-2026a}{number of elements} $|X|$ and \reftext{def:finite-set-2026a}{finite} be as in those definitions. Then the following hold.

1. For every $n\in\mathbb{N}$ the set $[n]$ has $n$ elements.
2. For every object $x$ the set $\{x\}$ has $1$ element. If $A$ has $k$ elements and $x\notin A$, then $A\cup\{x\}$ has $S(k)$ elements.
3. If $X$ is finite and $A\subseteq X$, then $A$ is finite. If moreover $X$ has $n$ elements and $A\ne\emptyset$, then $A$ has $m$ elements for some $m\le n$.
4. If $X$ has $n$ elements, $Y$ is a set, and $q:X\to Y$ is surjective (that is, every $y\in Y$ equals $q(x)$ for some $x\in X$), then $Y$ has $m$ elements for some $m\le n$; in particular $Y$ is finite and nonempty.