A D264: Semigroup $G = (X, +)$ is a monoid if and only if \begin{equation} \exists \, 0_G \in X : \forall \, x \in X : 0_G + x = x + 0_G = x \end{equation}