76/160
\begin{frame}{Reminder: Model Cardinality}
  Define $\aformi{n}$ for $n\in\nat$ with $n \ge 2$:
  \begin{talign}
    \aformi{n} \;=\;
       \displaystyle\formula{\existsst{x_1}{\ldots\existsst{x_{n}}{
           \bigwedge_{1\le i < j\le n}  \notequalto{x_i}{x_j}
       }}}
  \end{talign}

  Define $\bformi{n}$ for $n \in \nat$ with $n \ge 1$:
  \begin{talign}
    \bformi{n} \;=\;  
           \displaystyle\formula{ \forallst{x_1}{\ldots\forallst{x_{n+1}}{
             \bigvee_{1\le i < j\le n}  \equalto{x_i}{x_j}
           }}}
  \end{talign}

  \begin{proposition}
    For all models $\model{\amodel}$ and all $\forestgreen{n}\ge 2$ it holds:
    \begin{enumerate}[(i)]
      \item
        $\model{\amodel} \satisfies \aformi{\forestgreen{n}}
         \;\;\Longleftrightarrow\;\;
         \text{$\model{\adomain}$ has \alert{at least} $\forestgreen{n}$ elements}$
         (i.e.\ $\cardinality{\model{\adomain}} \ge \forestgreen{n}$)
      \item
        $\model{\amodel} \satisfies \bformi{\forestgreen{n}}
         \;\;\Longleftrightarrow\;\;
         \text{$\model{\adomain}$ has \alert{at most} $\forestgreen{n}$ elements}$
         (i.e.\ $\cardinality{\model{\adomain}} \le \forestgreen{n}$)
      \item
        $\model{\amodel} \satisfies \formula{\aformi{\forestgreen{n}} \logandinf \bformi{\forestgreen{n}}}
         \;\;\Longleftrightarrow\;\;
         \text{$\model{\adomain}$ has \alert{precisely} $\forestgreen{n}$ elements}$
         ($\cardinality{\model{\adomain}} = \forestgreen{n}$)
    \end{enumerate}
  \end{proposition}
\end{frame}