Theorem: Meet Preserves Directed Suprema

Let $\mathscr S = \struct {S, \preceq}$ be an up-complete meet semilattice such that
:$\forall x \in S$, a directed subset $D$ of $S$: $x \preceq \sup D \implies x \preceq \sup \set {x \wedge y: y \in D}$

Proof:
=== Lemma 2 ===
{{:Meet Preserves Directed Suprema/Lemma 2}}{{qed|lemma}}
Let $X$ be a directed subset of $S \times S$ such that
:$X$ admits a supremum.
By Up-Complete Product:
:the simple order product of $\mathscr S$ and $\mathscr S$ is up-complete.
By Up-Complete Product/Lemma 2:
:$X_1 := \map {\pr_1^\to} X$ is directed
and
:$X_2 := \map {\pr_2^\to} X$ is directed
where
:$\pr_1$ denotes the first projection on $S \times S$
:$\pr_2$ denotes the second projection on $S \times S$
:$\map {\pr_1^\to} X$ denotes the image of $X$
We will prove that
:$(1): \quad \set {x \wedge \sup X_2: x \in X_1} = \set {\sup \set {x \wedge y: y \in X_2}: x \in X_1}$
'''First inclusion:'''
Let $a \in \set {x \wedge \sup X_2: x \in X_1}$.
Then
:$\exists x \in X: a = x \wedge \sup X_2$
By Meet Precedes Operands:
:$x \wedge \sup X_2 \preceq \sup X_2$
By assumption:
:$x \wedge \sup X_2 \preceq \sup \set {x \wedge \sup X_2 \wedge y: y \in X_2}$
By definition of supremum:
:$\forall y \in X_2: y \preceq \sup X_2$
By Preceding iff Meet equals Less Operand:
:$\forall y \in X_2: \sup X_2 \wedge y = y$
By Meet is Associative:
:$x \wedge \sup X_2 \preceq \sup \set {x \wedge y: y \in X_2}$
By Meet Semilattice is Ordered Structure:
:$\forall y \in X_2: x \wedge y \preceq x \wedge \sup X_2$
By definition:
:$x \wedge \sup X_2$ is upper bound for $\set {x \wedge y: y \in X_2}$
By definition of supremum:
:$\sup \set {x \wedge y: y \in X_2} \preceq x \wedge \sup X_2$
By definition of antisymmetry:
:$a = \sup \set {x \wedge y: y \in X_2}$
Thus
:$a \in \set {\sup \set {x \wedge y: y \in X_2}: x \in X_1}$
{{qed|lemma}}
'''Second inclusion'''
Let $a \in \set {\sup \set {x \wedge y: y \in X_2}: x \in X_1}$.
Then
:$\exists x \in X_1: a = \sup \set {x \wedge y: y \in X_2}$
Analogically to first inclusion
:$a = x \wedge \sup X_2$
Thus
:$a \in \set {x \wedge \sup X_2: x \in X_1}$
{{qed|lemma}}
We will prove as lemma that:
:$\paren {\map {f^\to} X}$ is directed.
Let $x, y \in \paren {\map {f^\to} X}$.
By image of set:
:$\exists \tuple {a, b} \in X: x = \map f {a, b}$
and
:$\exists \tuple {c, d} \in X: y = \map f {c, d}$
By definition of $f$:
:$x = a \wedge b$ and $y = c \wedge d$
By definition of directed subset:
:$\exists \tuple {g, h} \in X: \tuple {a, b} \precsim \tuple {g, h} \land \tuple {c, d} \precsim \tuple {g, h}$
By simple order product:
:$a \preceq g$, $b \preceq h$, $c \preceq g$, and $d \preceq h$
By Meet Semilattice is Ordered Structure:
:$x \preceq g \wedge h$ and $y \preceq g \wedge h$
By definition of image of set:
:$g \wedge h = \map f {g, h} \in \map {f^\to} X$
Thus:
:$\exists z \in \map {f^\to} X: x \preceq z \land y \preceq z$
This ends the proof of lemma.
Thus by definition of up-complete:
:$\paren {\map {f^\to} X}$ admits a supremum.
Thus
{{begin-eqn}}
{{eqn | l = \map \sup {\map {f^\to} X}
      | r = \sup \set {x \wedge y: x \in X_1, y \in X_2}
      | c = Supremum of Meet Image of Directed Set
}}
{{eqn | r = \sup \bigcup \set {\set {x \wedge y: y \in X_2}: x \in X_1}
}}
{{eqn | r = \sup \set {\sup \set {x \wedge y: y \in X_2}: x \in X_1}
      | c = Supremum of Suprema
}}
{{eqn | r = \sup \set {x \wedge \sup X_2: x \in X_1}
      | c = the equality $(1)$
}}
{{eqn | r = \paren {\sup X_1} \wedge \paren {\sup X_2}
      | c = Lemma 2
}}
{{eqn | r = \map f {\sup X_1, \sup X_2}
      | c = Definition of $f$
}}
{{eqn | r = \map f {\sup X}
      | c = Supremum by Suprema of Directed Set in Simple Order Product
}}
{{end-eqn}}
{{qed}}