開近傍系は基本近傍系

開近傍系$ \mathcal N(x)\cap\mathcal Oは基本近傍系である

証明

$ \forall x\in X\forall N:

$ N\in\mathcal N(x)

$ \iff x\in N^\circ\land N\in2^X

$ \because$ \mathcal N(x)=\{N\in2^X|x\in N^\circ\}

$ \iff\exist O\in\mathcal O:x\in O\subseteq N\subseteq X

$ \iff\exist O\in\mathcal O_{\ni x}:O\subseteq N\subseteq X

$ \iff\exist O\in\mathcal N(x)\cap\mathcal O:O\subseteq N\subseteq X

$ \because\mathcal N(x)\cap\mathcal O=\{N\in\mathcal O|x\in N^\circ\}

$ = \{N\in\mathcal O|x\in N\}

$ \because\forall O\in\mathcal O:O^\circ=O

$ =\mathcal O_{\ni x}

$ \implies\exist N^*\in\mathcal N(x)\cap\mathcal O:N^*\subseteq N

$ \implies\forall x\in X\forall N\in\mathcal N(x)\exist N^*\in\mathcal N(x)\cap\mathcal O:N^*\subseteq N

$ \underline{\iff\forall x\in X:\mathcal N(x)\cap\mathcal O\text{は}x\text{の基本近傍系}\quad}_\blacksquare