Theorem: Way Below implies There Exists Way Below Open Filter Subset of Way Above Closure

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below continuous lattice.
Let $x, y \in S$ such that
:$x \ll y$
where $\ll$ denotes the way below relation.
Then there exists a way below open filter in $L$: $y \in F \land F \subseteq x^\gg$
where $x^\gg$ denotes the way above closure of $x$.

Proof:
We will prove that
:$x^\gg$ is way below open.
Let $z \in x^\gg$.
By definition of way above closure:
:$x \ll z$
By Way Below has Interpolation Property:
:$\exists x' \in S: x \ll x' \land x' \ll z$
Thus by definition of way above closure:
:$x' \in x^\gg$
Thus
:$x' \ll z$
{{qed|lemma}}
Then:
:$\forall z \in x^\gg: \exists y \in x^\gg: y \ll z$
By Axiom of Choice define a mapping $f: x^\gg \to x^\gg$:
:$\forall z \in x^\gg: \map f z \ll z$
By definition of way above closure:
:$y \in x^\gg$
Define $V := \set {z^\succeq: \exists n \in \N: z = \map {f^n} y}$
We will prove that
:$\forall X, Y \in V: \exists Z \in V: X \cup Y \subseteq Z$
Let $X, Y \in V$.
By definition of $V$:
:$\exists z_1 \in S: X = z_1^\succeq \land \exists n_1 \in \N: z_1 = \map {f^{n_1} } y$
and
:$\exists z_2 \in S: Y = z_2^\succeq \land \exists n_2 \in \N: z_2 = \map {f^{n_2} } y$
We will prove that
:$\forall n, k \in \N: \map {f^{n + k} } y \preceq \map {f^n} y$
Let $n \in \N$.
'''Base Case''':
By definition of reflexivity:
:$\map {f^{n + 0} } y \preceq \map {f^n} y$
'''Induction Hypothesis''':
:$\map {f^{n + k} } y \preceq \map {f^n} y$
'''Induction Step''':
By definition of $f$:
:$\map {f^{n + k + 1} } y \ll \map {f^{n + k} } y$
By Way Below implies Preceding:
:$\map {f^{n + k + 1} } y \preceq \map {f^{n + k} } y$
By Induction Hypothesis and definition of transitivity:
:$\map {f^{n + k + 1} } y \preceq \map {f^n} y$
{{qed|lemma}}
{{WLOG}}, suppose $n_1 \le n_2$
Then
:$\exists k \in \N: n_2 = n_1+k$
Then
:$z_2 \preceq z_1$
By Preceding iff Meet equals Less Operand:
:$z_1 \wedge z_2 = z_2$
By definition of $V$:
:$Z := \paren {z_1 \wedge z_2}^\succeq \in V$
By Meet Precedes Operands:
:$z_1 \wedge z_2 \preceq z_1$ and $z_1 \wedge z_2 \preceq z_2$
By Upper Closure is Decreasing:
:$z_1^\succeq \subseteq Z$ and $z_2^\succeq \subseteq Z$
Thus by Union of Subsets is Subset:
:$X \cup Y \subseteq Z$
{{qed|lemma}}
Define $F := \bigcup V$.
We will prove that
:$F$ is way below open.
Let $u \in F$.
By definition of union:
:$\exists Y \in V: u \in Y$
By definition of $V$:
:$\exists z \in S: Y = z^\succeq \land \exists n \in \N: z = \map {f^n} y$
By definition of $f$:
:$z \in x^\gg$
By definition of $f$:
:$\map f z \ll z$
Then
:$z' := \map f z = \map {f^{n + 1} } y$
By definition of $V$:
:${z'}^\succeq \in V$
By definition of reflexivity:
:$z' \preceq z'$
By definition of upper closure of element:
:$z' \in {z'}^\succeq$
By definition of union:
:$z' \in F$
By definition of upper closure of element:
:$z \preceq u$
By Preceding and Way Below implies Way Below:
:$z' \ll u$
Hence
:$\exists g \in F: g \ll u$
{{qed|lemma}}
By Upper Closure of Element is Filter:
:$\forall X \in V: X$ is a filtered upper section.
By Union of Upper Sections is Upper:
:$F$ is an upper section.
By Union of Filtered Sets is Filtered:
:$F$ is filtered.
By definition of filter:
:$F$ is a way below open filter in $L$.
Then:
:$\map {f^0} y = y$
By definition of $V$:
:$y^\succeq \in V$
By definitions of upper closure of element and reflexivity:
:$y \in y^\succeq$
By definition of union:
:$y \in F$
It remains to prove that
:$F \subseteq x^\gg$
Let $u \in F$.
By definition of union:
:$\exists Y \in V: u \in Y$
By definition of $V$:
:$\exists z \in S: Y = z^\succeq \land \exists n \in \N: z = \map {f^n} y$
By definition of $f$:
:$z \in x^\gg$
By definition of way above closure:
:$x \ll z$
By definition of upper closure of element:
:$z \preceq u$ and $x \preceq x$
By Preceding and Way Below implies Way Below:
:$x \ll u$
Thus by definition of way above closure:
:$u \in x^\gg$
{{qed}}