開核公理系→開集合系の公理

を導く

$ \begin{dcases}\text{(I1) }X^\circ =X\\\text{(I2) }\forall A\in2^X:A^\circ\subseteq A\\\text{(I3) }\forall A,B\in2^X:(A\cap B)^\circ=A^\circ\cap B^\circ\\\text{(I4) }\forall A\in2^X:{A^\circ}^\circ=A^\circ\\\text{(I0) }\mathcal O=\Set{O\in2^X|O^\circ=O}\end{dcases}\implies\begin{dcases}\text{(O1) }X\in\mathcal O\\\text{(O2) }\forall\mathcal O'\subseteq\mathcal O:\bigcup\mathcal O'\in\mathcal O\\\text{(O3) }\forall O_1,O_2\in\mathcal O:O_1\cap O_2\in\mathcal O\\\text{(O0) }\bullet^\circ:2^X\ni A\mapsto\max\left(\mathcal O\cap2^A\right)\end{dcases}

proof

$ x\in\max\left(\mathcal O\cap2^A\right)

$ \iff\exist O\in\mathcal O\cap2^A:x\in O

$ \iff\exist O\subseteq A:x\in O=O^\circ

$ \iff\exist O:x\in O^\circ=O\subseteq A^\circ\subseteq A

$ \implies x\in A^\circ

$ \iff x\in A^\circ={A^\circ}^\circ

$ \iff x\in A^\circ\in\mathcal O

$ \iff\exist O\in\mathcal O:x\in O=A^\circ\subseteq A

$ \iff\exist O\in\mathcal O\cap2^A:x\in O=A^\circ

$ \implies\exist O\in\mathcal O\cap2^A:x\in O

$ \iff x\in\max\left(\mathcal O\cap2^A\right)

$ \underline{\therefore\forall A\in2^X:A^\circ=\max\left(\mathcal O\cap2^A\right)\quad}_\blacksquare