# Complement of Subset with Property (S) is Closed under Directed Suprema

Jump to navigation
Jump to search

## Theorem

Let $L = \left({S, \preceq}\right)$ be an up-complete ordered set.

Let $X$ be a subset of $S$ with property (S).

Then $\complement_S\left({X}\right)$ is closed under directed suprema.

## Proof

Let $D$ be a directed subset of $S$ such that

- $D \subseteq \complement_S\left({X}\right)$

Aiming for a contradiction suppose that

- $\sup D \notin \complement_S\left({X}\right)$

By definition of relative complement:

- $\sup D \in X$

By definition of property (S):

- $\exists y \in D: \forall x \in D: y \preceq x \implies x \in X$

By definition of reflexivity:

- $y \in X$

By definitions of intersection and non-empty:

- $D \cap X \ne \varnothing$

Thus this by Empty Intersection iff Subset of Complement contradicts

- $D \subseteq \complement_S\left({X}\right)$

$\blacksquare$

## Sources

- Mizar article WAYBEL11:funcreg 1