\begin{definition}[Definition:Cardinality/Finite]
Let $S$ be a finite set.
The '''cardinality''' $\card S$ of $S$ is the '''number of elements in $S$'''.
That is, if:
:$S \sim \N_{< n}$
where:
:$\sim$ denotes set equivalence
:$\N_{<n}$ is the set of all natural numbers less than $n$
then we define:
:$\card S = n$
Also note that from the definition of finite:
:$\exists n \in \N: \card S = n \iff S$ is finite.
\end{definition}