Peeling an Element off a Finite Set, and Unions of Finite Sets

Let $\mathbb{N}$ be the set of natural numbers with successor map $S$ as in that definition, ordered by the relations of Order on the Natural Numbers, and for $p\in\mathbb{N}$ let $[p]$ be the initial segment determined by $p$. The notions has $k$ elements and finite are those of the indicated definitions.

Then the following hold.

1. (Adjoining a point) If $C$ is a finite set and $x$ is an object, then $C\cup\{x\}$ is finite.

2. (Peeling) Let $k\in\mathbb{N}$ and let $B$ be a set with $S(k)$ elements. Then there are a subset $B'\subseteq B$ with $k$ elements and an element $x\in B$ with $x\notin B'$ such that $B=B'\cup\{x\}$.

3. (Unions) If $A$ and $B$ are finite sets, then $A\cup B$ is finite.