冪集合の単項filter
任意の集合$ Xについて$ \mathcal \uparrow:2^X\ni U\mapsto\{F\in2^X|U\subseteq F\}\in 2^Xとしたとき、$ \uparrow Uは$ (2^X,\subseteq)のfilter (数学)となる $ \uparrow Uが有限交叉性を持つことと、(17-1)を満たすことを同時並行で示す $ \forall\mathcal F'\subseteq 2^X.
$ \mathcal F'\subseteq\uparrow U
$ \iff\forall F\in\mathcal F'.F\in\uparrow U
$ \iff\forall F\in\mathcal F'.U\subseteq F
$ \iff U\subseteq\mathcal F'ー☆
$ \iff\begin{dcases}U\subseteq\bigcap\mathcal F'\\\forall V\in2^X.\end{dcases}
$ \bigcap\mathcal F'\subseteq V
$ \implies U\subseteq V\quad\because☆
$ \iff V\in\uparrow U
$ \iff\begin{dcases}U\subseteq\bigcap\mathcal F'\\\forall V\in2^X.(\bigcap\mathcal F'\subseteq V\implies V\in\uparrow U)\end{dcases}
$ \implies\begin{dcases}\bigcap\mathcal F'\neq\varnothing\\\forall V\in2^X.(\bigcap\mathcal F'\subseteq V\implies V\in\uparrow U)\end{dcases}
$ \implies\forall\mathcal F'\subseteq\uparrow U.\begin{dcases}\bigcap\mathcal F'\neq\varnothing\\\forall V\in 2^X.(\bigcap\mathcal F'\subseteq V\implies V\in\uparrow U)\end{dcases}
$ \implies\forall\mathcal F'\subseteq\uparrow U.\left(|\mathcal F'|\in\Z_{\ge0}\implies\begin{dcases}\bigcap\mathcal F'\neq\varnothing\\\forall V\in 2^X.(\bigcap\mathcal F'\subseteq V\implies V\in\uparrow U)\end{dcases}\right)