Bottom in Ordered Set of Topology

Theorem

Let $T = \struct {S, \tau}$ be a topological space.

Let $P = \struct {\tau, \subseteq}$ be an inclusion ordered set of $\tau$.

Then $P$ is bounded below and $\bot_P = \O$

Proof

By Empty Set is Element of Topology:

$\O \in \tau$

By Empty Set is Subset of All Sets:

$\forall A \in \tau: \O \subseteq A$

Hence $P$ is bounded below.

Thus by definition of the smallest element:

$\bot_P = \O$

$\blacksquare$

Sources

• Mizar article YELLOR_1:23