# Top in Ordered Set of Topology

Jump to navigation
Jump to search

## 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