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

$ \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{(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\end{dcases}

proof

$ \underline{\implies X\in\mathcal O\quad}_\blacksquare

$ \implies\forall x:

$ x\in\bigcup\mathcal O'

$ \iff\exist O\in\mathcal O':x\in O

$ \iff\exist O:x\in O\land\Set{O}\subseteq\mathcal O'

$ \implies\exist O:x\in O\subseteq\bigcup\mathcal O'

$ \implies\exist O:x\in O^\circ\subseteq\left(\bigcup\mathcal O'\right)^\circ

$ \implies x\in\left(\bigcup\mathcal O'\right)^\circ

$ \subseteq\bigcup\mathcal O'

$ \implies\bigcup\mathcal O'=\left(\bigcup\mathcal O'\right)^\circ

$ \iff \bigcup\mathcal O'\in\mathcal O

$ \underline{\therefore\forall\mathcal O'\subseteq\mathcal O:\bigcup\mathcal O'\in\mathcal O\quad}_\blacksquare

$ \iff\begin{dcases}{O_1}^\circ=O_1\\{O_2}^\circ=O_2\end{dcases}

$ \implies O_1\cap O_2={O_1}^\circ\cap{O_2}^\circ

$ =(O_1\cap O_2)^\circ

$ \implies O_1\cap O_2\in\mathcal O

$ \underline{\therefore\forall O_1,O_2\in\mathcal O:O_1\cap O_2\in\mathcal O\quad}_\blacksquare