\begin{definition}[Definition:Finite Group]
A '''finite group''' is a group of finite order.
That is, a group $\struct {G, \circ}$ is a '''finite group''' {{iff}} its underlying set $G$ is finite.
That is, a '''finite group''' is a group with a finite number of elements.
\end{definition}