Top in Ordered Set of Topology

Theorem

Let $T = \left({S, \tau}\right)$ be a topological space.

Let $P = \left({\tau, \subseteq}\right)$ be an inclusion ordered set of $\tau$.

Then $P$ is bounded above and $\top_P = S$

where $\top_P$ denotes the greatest element in $P$.

Proof

By definition of topological space:

$S \in \tau$

By definition of subset:

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

Hence $P$ is bounded above.

Thus by definition of the greatest element:

$\top_P = S$

$\blacksquare$

Sources

• Mizar article YELLOR_1:24