Hausdorffの公理系→Kuratowskiの閉包公理系

証明

$ =\{x\in X\mid\bot\}

$ \underline{=\varnothing\quad}_\blacksquare

$ x\in A

$ \iff x\in A\land\forall N\in\mathcal N(x):x\in N

$ \implies\forall N\in\mathcal N(x):N\cap A\neq\varnothing

$ \iff x\in\overline{A}

$ \underline{\therefore\forall A\in2^X:A\subseteq\overline{A}\quad}_\blacksquare

$ x\in\overline{\overline{A}}

$ \iff\forall N\in\mathcal N(x):N\cap\overline{A}\neq\varnothing

$ \iff\forall N\in\mathcal N(x)\exist y\in N\forall O\in\mathcal N(y):O\cap A\neq\varnothing

$ x\in\overline{A\cup B}

$ \iff\forall N\in\mathcal N(x):N\cap(A\cup B)\neq\varnothing

$ \iff\forall N\in\mathcal N(x):N\cap A\neq\varnothing\land N\cap B\neq\varnothing

$ \iff x\in\overline{A}\cup\overline{B}

$ \underline{\therefore\forall A,B\in2^X:\overline{A\cup B}=\overline{A}\cup\overline{B}\quad}_\blacksquare

$ \forall A\in2^X\forall x:

$ x\in\overline{A}

$ \iff x\notin X\setminus\overline{X\setminus (X\setminus A)}

$ \iff X\setminus A\notin\mathcal N(x)

$ \iff x\in X\land X\setminus A\notin\mathcal N(x)

$ \iff x\in X\land 2^{X\setminus A}\cap\mathcal N(x)=\varnothing

$ \iff x\in X\land\lnot\exist N\in\mathcal N(x):N\in2^{X\setminus A}

$ \iff x\in X\land\forall N\in\mathcal N(x):N\notin2^{X\setminus A}

$ \iff x\in X\land\forall N\in\mathcal N(x):N\nsubseteq X\setminus A

$ \iff x\in X\land\forall N\in\mathcal N(x):\lnot(X\setminus A=(X\setminus A)\cup N)

$ \iff x\in X\land\forall N\in\mathcal N(x):\lnot(A=X\setminus((X\setminus A)\cup N))

$ \iff x\in X\land\forall N\in\mathcal N(x):\lnot(A=A\cap (X\setminus N))

$ \iff x\in X\land\forall N\in\mathcal N(x):\lnot(A\subseteq X\setminus N)

$ \iff x\in X\land\forall N\in\mathcal N(x):N\cap A\neq\varnothing

$ \iff x\in\{x\in X\mid\forall N\in\mathcal N(x):N\cap A\neq\varnothing\}

$ \underline{\implies\forall A\in2^X:\overline A=\{x\in X\mid\forall N\in\mathcal N(x):N\cap A\neq\varnothing\}\quad}_\blacksquare