Closed Subset is Upper Section in Lower Topology

Theorem

Let $T = \struct {S, \preceq, \tau}$ be a transitive relational structure with lower topology.

Let $A \subseteq S$ such that

$A$ is closed.

Then $A$ is an upper section of $S$.

Proof

By definition of closed set:

$S \setminus A$ is open.

By Open Subset is Lower Section in Lower Topology:

$S \setminus A$ is a lower section.

Thus by Complement of Lower Section is Upper Section and Relative Complement of Relative Complement:

$A$ is an upper section of $S$.

$\blacksquare$

Sources

• Mizar article WAYBEL19:6