以下逐條檢定拓撲 的定義：
(1) 等價於「
X
∈
U
{\displaystyle X\in {\mathcal {U}}}
若
X
∈
U
{\displaystyle X\in {\mathcal {U}}}
(
∃
A
)
[
(
A
⊆
F
)
∧
(
⋃
A
=
X
)
]
{\displaystyle (\exists {\mathcal {A}})\left[({\mathcal {A}}\subseteq {\mathcal {F}})\wedge \left(\bigcup {\mathcal {A}}=X\right)\right]}
考慮到
F
⊆
P
(
X
)
{\displaystyle {\mathcal {F}}\subseteq {\mathcal {P}}(X)}
無限聯集性質 的定理(1)與(2)有
⋃
F
⊆
X
{\displaystyle \bigcup {\mathcal {F}}\subseteq X}
但根據無限聯集性質 的定理(1)，(a)又等價於：
(
∃
A
)
[
(
A
⊆
F
)
∧
(
⋃
A
=
X
)
∧
(
⋃
A
⊆
⋃
F
)
]
{\displaystyle (\exists {\mathcal {A}})\left[({\mathcal {A}}\subseteq {\mathcal {F}})\wedge \left(\bigcup {\mathcal {A}}=X\right)\wedge \left(\bigcup {\mathcal {A}}\subseteq \bigcup {\mathcal {F}}\right)\right]}
所以有：
X
⊆
⋃
F
{\displaystyle X\subseteq \bigcup {\mathcal {F}}}
所以從
X
∈
U
{\displaystyle X\in {\mathcal {U}}}
⋃
F
=
X
{\displaystyle \bigcup {\mathcal {F}}=X}
反之若有 (a1)，因為
F
⊆
F
{\displaystyle {\mathcal {F}}\subseteq {\mathcal {F}}}
X
∈
U
{\displaystyle X\in {\mathcal {U}}}
X
∈
U
{\displaystyle X\in {\mathcal {U}}}
(2)
∅
∈
U
{\displaystyle \varnothing \in {\mathcal {U}}}
首先考慮到
∅
⊆
F
{\displaystyle \varnothing \subseteq {\mathcal {F}}}
無限聯集性質 的定理(0)有
∅
=
⋃
∅
{\displaystyle \varnothing =\bigcup \varnothing }
∅
∈
U
{\displaystyle \varnothing \in {\mathcal {U}}}
(3) 對任意
A
⊆
U
{\displaystyle {\mathfrak {A}}\subseteq {\mathcal {U}}}
⋃
A
∈
U
{\displaystyle \bigcup {\mathfrak {A}}\in {\mathcal {U}}}
首先，
A
⊆
U
{\displaystyle {\mathfrak {A}}\subseteq {\mathcal {U}}}
(
∀
A
∈
A
)
(
∃
B
)
[
(
B
⊆
F
)
∧
(
⋃
B
=
A
)
]
{\displaystyle (\forall A\in {\mathfrak {A}})(\exists {\mathcal {B}})\left[({\mathcal {B}}\subseteq {\mathcal {F}})\wedge \left(\bigcup {\mathcal {B}}=A\right)\right]}
上式可直觀地解釋成「
A
∈
A
{\displaystyle A\in {\mathfrak {A}}}
F
{\displaystyle {\mathcal {F}}}
聯集 」，既然如此，取一個蒐集各種不同
A
{\displaystyle A}
子集 的集族
P
A
{\displaystyle {\mathcal {P}}_{\mathfrak {A}}}
P
A
:=
{
S
|
(
∃
A
)
[
(
A
∈
A
)
∧
(
S
⊆
A
)
]
}
{\displaystyle {\mathcal {P}}_{\mathfrak {A}}:=\left\{S\,|\,(\exists A)[(A\in {\mathfrak {A}})\wedge (S\subseteq A)]\right\}}
這樣根據有限交集 的性質，
x
∈
⋃
(
P
A
∩
F
)
{\displaystyle x\in \bigcup ({\mathcal {P}}_{\mathfrak {A}}\cap {\mathcal {F}})}
(
∃
S
)
{
(
x
∈
S
)
∧
(
S
∈
F
)
∧
(
∃
A
)
[
(
A
∈
A
)
∧
(
S
⊆
A
)
]
}
{\displaystyle (\exists S)\left\{(x\in S)\wedge (S\in {\mathcal {F}})\wedge (\exists A)\left[(A\in {\mathfrak {A}})\wedge (S\subseteq A)\right]\right\}}
考慮到一階邏輯 的定理(Ce) ，將
(
∃
A
)
{\displaystyle (\exists A)}
(
∃
S
)
{\displaystyle (\exists S)}
(Equv) 而等價於
(
∃
A
)
{
(
A
∈
A
)
∧
(
∃
S
)
[
(
x
∈
S
)
∧
(
S
∈
F
)
∧
(
S
⊆
A
)
]
}
{\displaystyle (\exists A)\left\{(A\in {\mathfrak {A}})\wedge (\exists S)\left[(x\in S)\wedge (S\in {\mathcal {F}})\wedge (S\subseteq A)\right]\right\}}
也就等價於
(
∃
A
)
{
(
A
∈
A
)
∧
(
x
∈
⋃
[
P
(
A
)
∩
F
]
)
}
{\displaystyle (\exists A)\left\{(A\in {\mathfrak {A}})\wedge \left(x\in \bigcup [{\mathcal {P}}(A)\cap {\mathcal {F}}]\right)\right\}}
根據無限聯集性質 的定理(4)，從(b)有
(
∀
A
∈
A
)
(
∃
B
)
{
(
B
⊆
F
)
∧
{
A
⊆
⋃
[
B
∩
P
(
A
)
]
}
}
{\displaystyle (\forall A\in {\mathfrak {A}})(\exists {\mathcal {B}})\left\{({\mathcal {B}}\subseteq {\mathcal {F}})\wedge \left\{A\subseteq \bigcup [{\mathcal {B}}\cap {\mathcal {P}}(A)]\right\}\right\}}
這樣根據無限聯集性質 的定理(1)又會有
(
∀
A
∈
A
)
{
A
⊆
⋃
[
F
∩
P
(
A
)
]
}
{\displaystyle (\forall A\in {\mathfrak {A}})\left\{A\subseteq \bigcup [{\mathcal {F}}\cap {\mathcal {P}}(A)]\right\}}
考慮到
F
∩
P
(
A
)
⊆
P
(
A
)
{\displaystyle {\mathcal {F}}\cap {\mathcal {P}}(A)\subseteq {\mathcal {P}}(A)}
無限聯集性質 的定理(1)與定理(2)有
⋃
F
∩
P
(
A
)
⊆
A
{\displaystyle \bigcup {\mathcal {F}}\cap {\mathcal {P}}(A)\subseteq A}
所以最後從(b)有
(
∀
A
∈
A
)
{
A
=
⋃
[
F
∩
P
(
A
)
]
}
{\displaystyle (\forall A\in {\mathfrak {A}})\left\{A=\bigcup [{\mathcal {F}}\cap {\mathcal {P}}(A)]\right\}}
所以
x
∈
⋃
(
P
A
∩
F
)
{\displaystyle x\in \bigcup ({\mathcal {P}}_{\mathfrak {A}}\cap {\mathcal {F}})}
(
∃
A
)
[
(
A
∈
A
)
∧
(
x
∈
A
)
]
{\displaystyle (\exists A)\left[(A\in {\mathfrak {A}})\wedge (x\in A)\right]}
換句話說
x
∈
⋃
A
{\displaystyle x\in \bigcup {\mathfrak {A}}}
這樣考慮到
P
A
∩
F
⊆
F
{\displaystyle {\mathcal {P}}_{\mathfrak {A}}\cap {\mathcal {F}}\subseteq {\mathcal {F}}}
⋃
A
=
⋃
(
P
A
∩
F
)
∈
U
{\displaystyle \bigcup {\mathfrak {A}}=\bigcup ({\mathcal {P}}_{\mathfrak {A}}\cap {\mathcal {F}})\in {\mathcal {U}}}
所以在本定理的前提下， 對所有
A
⊆
U
{\displaystyle {\mathfrak {A}}\subseteq {\mathcal {U}}}
⋃
A
∈
U
{\displaystyle \bigcup {\mathfrak {A}}\in {\mathcal {U}}}
(4)等價於「
U
,
V
∈
U
{\displaystyle U,\,V\in {\mathcal {U}}}
U
∩
V
∈
U
{\displaystyle U\cap V\in {\mathcal {U}}}
若
「對所有的
U
,
V
∈
U
{\displaystyle U,\,V\in {\mathcal {U}}}
U
∩
V
∈
U
{\displaystyle U\cap V\in {\mathcal {U}}}
因取任意
B
1
,
B
2
∈
F
{\displaystyle B_{1},\,B_{2}\in {\mathcal {F}}}
B
1
=
⋃
{
B
1
}
∈
U
{\displaystyle B_{1}=\bigcup \{B_{1}\}\in {\mathcal {U}}}
B
2
=
⋃
{
B
1
}
∈
U
{\displaystyle B_{2}=\bigcup \{B_{1}\}\in {\mathcal {U}}}
故
B
1
∩
B
2
∈
U
{\displaystyle B_{1}\cap B_{2}\in {\mathcal {U}}}
「對所有
B
1
,
B
2
∈
F
{\displaystyle B_{1},\,B_{2}\in {\mathcal {F}}}
B
1
∩
B
2
∈
U
{\displaystyle B_{1}\cap B_{2}\in {\mathcal {U}}}
另一方面，
U
∩
V
∈
U
{\displaystyle U\cap V\in {\mathcal {U}}}
(
∃
E
)
{
(
E
⊆
F
)
∧
(
U
∩
V
=
⋃
E
)
}
{\displaystyle (\exists {\mathcal {E}})\left\{({\mathcal {E}}\subseteq {\mathcal {F}})\wedge \left(U\cap V=\bigcup {\mathcal {E}}\right)\right\}}
因為
U
,
V
∈
U
{\displaystyle U,\,V\in {\mathcal {U}}}
(
∃
A
)
[
(
U
=
⋃
A
)
∧
(
A
⊆
F
)
]
{\displaystyle (\exists {\mathcal {A}})\left[\left(U=\bigcup {\mathcal {A}}\right)\wedge ({\mathcal {A}}\subseteq {\mathcal {F}})\right]}
(
∃
B
)
[
(
V
=
⋃
B
)
∧
(
B
⊆
F
)
]
{\displaystyle (\exists {\mathcal {B}})\left[\left(V=\bigcup {\mathcal {B}}\right)\wedge ({\mathcal {B}}\subseteq {\mathcal {F}})\right]}
所以在
U
,
V
∈
U
{\displaystyle U,\,V\in {\mathcal {U}}}
U
∩
V
∈
U
{\displaystyle U\cap V\in {\mathcal {U}}}
(
∃
A
)
(
∃
B
)
(
∃
E
)
{
(
A
,
B
,
E
⊆
F
)
∧
(
U
=
⋃
A
)
∧
(
V
=
⋃
B
)
∧
[
(
⋃
A
)
∩
(
⋃
B
)
=
⋃
E
]
}
{\displaystyle (\exists {\mathcal {A}})(\exists {\mathcal {B}})(\exists {\mathcal {E}})\left\{({\mathcal {A}},\,{\mathcal {B}},\,{\mathcal {E}}\subseteq {\mathcal {F}})\wedge \left(U=\bigcup {\mathcal {A}}\right)\wedge \left(V=\bigcup {\mathcal {B}}\right)\wedge \left[\left(\bigcup {\mathcal {A}}\right)\cap \left(\bigcup {\mathcal {B}}\right)=\bigcup {\mathcal {E}}\right]\right\}}
此時考慮到一階邏輯 的定理(Ce) ，連續使用兩次會有：
[
x
∈
(
⋃
A
)
∩
(
⋃
B
)
]
⇔
(
∃
A
)
(
∃
B
)
[
(
A
∈
A
)
∧
(
B
∈
B
)
∧
(
x
∈
A
∩
B
)
]
{\displaystyle \left[x\in \left(\bigcup {\mathcal {A}}\right)\cap \left(\bigcup {\mathcal {B}}\right)\right]\Leftrightarrow (\exists A)(\exists B)[(A\in {\mathcal {A}})\wedge (B\in {\mathcal {B}})\wedge (x\in A\cap B)]}
這樣的話，若取一個包含所有
A
∩
B
{\displaystyle A\cap B}
C
:=
{
S
∈
P
(
X
)
|
(
∃
A
)
(
∃
B
)
[
(
A
∈
A
)
∧
(
B
∈
B
)
∧
(
S
=
A
∩
B
)
]
}
{\displaystyle {\mathcal {C}}:=\left\{S\in {\mathcal {P}}(X)\,{\big |}\,(\exists A)(\exists B)[(A\in {\mathcal {A}})\wedge (B\in {\mathcal {B}})\wedge (S=A\cap B)]\right\}}
這樣就有：
⋃
C
=
(
⋃
A
)
∩
(
⋃
B
)
{\displaystyle \bigcup {\mathcal {C}}=\left(\bigcup {\mathcal {A}}\right)\cap \left(\bigcup {\mathcal {B}}\right)}
而且考慮到
A
⊆
F
{\displaystyle {\mathcal {A}}\subseteq {\mathcal {F}}}
B
⊆
F
{\displaystyle {\mathcal {B}}\subseteq {\mathcal {F}}}
A
∩
B
{\displaystyle A\cap B}
U
{\displaystyle {\mathcal {U}}}
C
⊆
U
{\displaystyle {\mathcal {C}}\subseteq {\mathcal {U}}}
U
∩
V
∈
U
{\displaystyle U\cap V\in {\mathcal {U}}}
所以，(P')跟(P)等價 。
綜合上面的(a1)、(a2)、和(P')，本定理得證。
◻
{\displaystyle \Box }
![{\displaystyle {\mathcal {U}}:=\left\{U\in {\mathcal {P}}(X)\,{\bigg |}\,(\exists {\mathcal {A}})\left[({\mathcal {A}}\subseteq {\mathcal {F}})\wedge \left(\bigcup {\mathcal {A}}=U\right)\right]\right\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6552c4bb1c9a261aa28f58b6d14e9ffb91718f9c)
![{\displaystyle \tau :=\left\{U\in {\mathcal {P}}(X)\,{\bigg |}\,(\exists {\mathcal {A}})\left[({\mathcal {A}}\subseteq {\mathcal {F}})\wedge \left(\bigcup {\mathcal {A}}=U\right)\right]\right\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e61f4036aae37167d3020340f8f3fda4ba97357f)
![{\displaystyle (\exists {\mathcal {A}})\left[({\mathcal {A}}\subseteq {\mathcal {F}})\wedge \left(\bigcup {\mathcal {A}}=X\right)\right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fee406497750030916f368f023fdc759dcd3025f)
![{\displaystyle (\exists {\mathcal {A}})\left[({\mathcal {A}}\subseteq {\mathcal {F}})\wedge \left(\bigcup {\mathcal {A}}=X\right)\wedge \left(\bigcup {\mathcal {A}}\subseteq \bigcup {\mathcal {F}}\right)\right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4048ceb87ca112eff7397bffe6ac16ef745dffa1)
![{\displaystyle (\forall A\in {\mathfrak {A}})(\exists {\mathcal {B}})\left[({\mathcal {B}}\subseteq {\mathcal {F}})\wedge \left(\bigcup {\mathcal {B}}=A\right)\right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/562c375929709e08d79865e9bb438fb98dc12af5)
![{\displaystyle {\mathcal {P}}_{\mathfrak {A}}:=\left\{S\,|\,(\exists A)[(A\in {\mathfrak {A}})\wedge (S\subseteq A)]\right\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/be768e1442ef0a1826cade8ea9e70c1749efed37)
![{\displaystyle (\exists S)\left\{(x\in S)\wedge (S\in {\mathcal {F}})\wedge (\exists A)\left[(A\in {\mathfrak {A}})\wedge (S\subseteq A)\right]\right\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9aa7c4580b7a64778683b76bdbee07cd1bfd9347)
![{\displaystyle (\exists A)\left\{(A\in {\mathfrak {A}})\wedge (\exists S)\left[(x\in S)\wedge (S\in {\mathcal {F}})\wedge (S\subseteq A)\right]\right\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ac3a18ea63ef91b939c27cddcc74ef2d1ce939f7)
![{\displaystyle (\exists A)\left\{(A\in {\mathfrak {A}})\wedge \left(x\in \bigcup [{\mathcal {P}}(A)\cap {\mathcal {F}}]\right)\right\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9f9f287ce7005814bf95f58735a6c4f77f6e903e)
![{\displaystyle (\forall A\in {\mathfrak {A}})(\exists {\mathcal {B}})\left\{({\mathcal {B}}\subseteq {\mathcal {F}})\wedge \left\{A\subseteq \bigcup [{\mathcal {B}}\cap {\mathcal {P}}(A)]\right\}\right\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/72e7dfa1a449ca1b00fb36ebd356e30b6bc90508)
![{\displaystyle (\forall A\in {\mathfrak {A}})\left\{A\subseteq \bigcup [{\mathcal {F}}\cap {\mathcal {P}}(A)]\right\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/02b70ec8450b58f630a1a31a99e1bfcd34d1cc93)
![{\displaystyle (\forall A\in {\mathfrak {A}})\left\{A=\bigcup [{\mathcal {F}}\cap {\mathcal {P}}(A)]\right\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/672b974565a53883ad9caf30ffaf25f62991d076)
![{\displaystyle (\exists A)\left[(A\in {\mathfrak {A}})\wedge (x\in A)\right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3d96c30244b847ae08f23ea4f0096b7a70781b7c)
![{\displaystyle (\exists {\mathcal {A}})\left[\left(U=\bigcup {\mathcal {A}}\right)\wedge ({\mathcal {A}}\subseteq {\mathcal {F}})\right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5659d1a94a17a8c2ef64f8d110fe396b19a68441)
![{\displaystyle (\exists {\mathcal {B}})\left[\left(V=\bigcup {\mathcal {B}}\right)\wedge ({\mathcal {B}}\subseteq {\mathcal {F}})\right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a480f645f5c7b2a5fd69de780873aa86200954df)
![{\displaystyle (\exists {\mathcal {A}})(\exists {\mathcal {B}})(\exists {\mathcal {E}})\left\{({\mathcal {A}},\,{\mathcal {B}},\,{\mathcal {E}}\subseteq {\mathcal {F}})\wedge \left(U=\bigcup {\mathcal {A}}\right)\wedge \left(V=\bigcup {\mathcal {B}}\right)\wedge \left[\left(\bigcup {\mathcal {A}}\right)\cap \left(\bigcup {\mathcal {B}}\right)=\bigcup {\mathcal {E}}\right]\right\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fc82e0d8e4ddea9b3fbbb6625dc2902b9fd84cd1)
![{\displaystyle \left[x\in \left(\bigcup {\mathcal {A}}\right)\cap \left(\bigcup {\mathcal {B}}\right)\right]\Leftrightarrow (\exists A)(\exists B)[(A\in {\mathcal {A}})\wedge (B\in {\mathcal {B}})\wedge (x\in A\cap B)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6b9677083fc0f9ea0eed46be3071a0f0278b444b)
![{\displaystyle {\mathcal {C}}:=\left\{S\in {\mathcal {P}}(X)\,{\big |}\,(\exists A)(\exists B)[(A\in {\mathcal {A}})\wedge (B\in {\mathcal {B}})\wedge (S=A\cap B)]\right\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9e51dd3a55a827fa811d179305edf37ab1a2fa06)
![{\displaystyle B_{1}\cap B_{2}=\bigcup [{\mathcal {F}}\cap {\mathcal {P}}(B_{1}\cap B_{2})]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b82402437fd6e3e7b061016c6834c53313301a28)
![{\displaystyle C\in [{\mathcal {F}}\cap {\mathcal {P}}(B_{1}\cap B_{2})]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1eb418fba4dfe4027244c2860b0431c3bb283cc2)
![{\displaystyle \vdash (\forall S){\big \{}[S\in \tau ({\mathcal {B}})]\Leftrightarrow (\forall {\mathfrak {T}})\{[({\mathfrak {T}}{\text{ is a topology of }}X)\wedge ({\mathcal {B}}\subseteq {\mathfrak {T}})]\Rightarrow (S\in {\mathfrak {T}})\}{\big \}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cac8fc52580d0b033c9c3524c4536a89bbe74b2d)
![{\displaystyle \vdash [S\in \tau ({\mathcal {B}})]\Leftrightarrow (\forall {\mathfrak {T}})\{[({\mathfrak {T}}{\text{ is a topology of }}X)\wedge ({\mathcal {B}}\subseteq {\mathfrak {T}})]\Rightarrow (S\in {\mathfrak {T}})\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5c06100e1e2ca6d6327e86ca739a966fb7125d6d)
![{\displaystyle \vdash [S\in \tau ({\mathcal {B}})]\Rightarrow \{[(\tau _{B}{\text{ is a topology of }}X)\wedge ({\mathcal {B}}\subseteq \tau _{B})]\Rightarrow (S\in \tau _{B})\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f85907e0b1f43e2f4954650bcf0073ea2d8552ea)
![{\displaystyle {\mathcal {P}}\vdash [S\in \tau ({\mathcal {B}})]\Rightarrow (S\in \tau _{B})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b5c919de46e07428d8df89a55e7e05e8e6e33e2a)
![{\displaystyle {\mathcal {P}},\,S\in \tau _{B}\vdash (\exists {\mathcal {C}})\left[\left(S=\bigcup {\mathcal {C}}\right)\wedge ({\mathcal {C}}\subseteq {\mathcal {B}})\right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ab602c5d3e55cd01619e2f8a318567675bf64f4e)
![{\displaystyle {\mathcal {P}},\,[({\mathfrak {T}}{\text{ is a topology of }}X)\wedge ({\mathcal {B}}\subseteq {\mathfrak {T}})],\,\left[\left(S=\bigcup {\mathcal {C}}\right)\wedge ({\mathcal {C}}\subseteq {\mathcal {B}})\right]\vdash (S\in {\mathfrak {T}})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/195d5e9c9b6ce324fcac759862f9f1e82b1f34d8)
![{\displaystyle {\mathcal {P}},\,[({\mathfrak {T}}{\text{ is a topology of }}X)\wedge ({\mathcal {B}}\subseteq {\mathfrak {T}})]\vdash (\exists C)\left[\left(S=\bigcup {\mathcal {C}}\right)\wedge ({\mathcal {C}}\subseteq {\mathcal {B}})\right]\Rightarrow (S\in {\mathfrak {T}})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/eaec5f769e9245dcc359da1c2b7761ccb9fac5c9)
![{\displaystyle {\mathcal {P}},\,S\in \tau _{B}\vdash [({\mathfrak {T}}{\text{ is a topology of }}X)\wedge ({\mathcal {B}}\subseteq {\mathfrak {T}})]\Rightarrow (S\in {\mathfrak {T}})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/51a1487b78aa2bfb0c189d15b94af55c31ebe9d5)
![{\displaystyle {\mathcal {P}},\,S\in \tau _{B}\vdash (\forall {\mathfrak {T}})\{[({\mathfrak {T}}{\text{ is a topology of }}X)\wedge ({\mathcal {B}}\subseteq {\mathfrak {T}})]\Rightarrow (S\in {\mathfrak {T}})\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/62c05ffd61c1317fd4d1fe4208459e3e1a351970)
![{\displaystyle {\mathcal {P}}\vdash (S\in \tau _{B})\Leftrightarrow [S\in \tau ({\mathcal {B}})]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2a024efc6d58b8ccc3eacdf657385486c1b1c239)
