Theorem: Continuous iff Mapping at Limit Inferior Precedes Limit Inferior of Composition of Mapping and Sequence

Let $\struct {S, \preceq_1, \tau_1}$ and $\struct {T, \preceq_2, \tau_2}$ be complete topological lattices with Scott topologies.
Let $f: S \to T$ be a mapping.
Then $f$ is continuous {{iff}}:
:for all directed set $\struct {D, \precsim}$ and net $N: D \to S$ in $S$: $\map f {\liminf N} \preceq_2 \map \liminf {f \circ N}$

Proof:
=== Sufficient Condition ===
Assume that
:$f$ is continuous.
Let $\struct {D, \precsim}$ be a directed set.
Let $N: D \to S$ be a net in $S$.
{{AimForCont}}
:$\map f {\liminf N} \npreceq_2 \map \liminf {f \circ N}$
By definition of lower closure of element:
:$\map f {\liminf N} \notin \paren {\map \liminf {f \circ N} }^{\preceq_2}$
By definition of relative complement:
:$\map f {\liminf N} \in \relcomp T {\paren {\map \liminf {f \circ N} }^{\preceq_2} }$
By Lower Closure of Element is Topologically Closed in Scott Topological Ordered Set:
:$\paren {\map \liminf {f \circ N} }^{\preceq_2}$ is closed.
By definition of closed set:
:$\relcomp T {\paren {\map \liminf {f \circ N} }^{\preceq_2} }$ is open.
By definition of continuous:
:$f^{-1} \sqbrk {\relcomp T {\paren {\map \liminf {f \circ N} }^{\preceq_2} } }$ is open.
By Open iff Upper and with Property (S) in Scott Topological Lattice:
:$f^{-1} \sqbrk {\relcomp T {\paren {\map \liminf {f \circ N} }^{\preceq_2} } }$ has property (S).
By Set of Infima for Sequence is Directed:
:$X := \set {\map \inf {N \sqbrk {\map \precsim j} }: j \in D}$ is directed.
By definition of limit inferior:
:$\liminf N = \sup X$
By definition of preimage of set:
:$\liminf N \in f^{-1} \sqbrk {\relcomp T {\paren {\map \liminf {f \circ N} }^{\preceq_2} } }$
By definition of property (S):
:$\exists y \in X:\forall x \in X: y \preceq_1 x \implies x \in f^{-1} \sqbrk {\relcomp T {\paren {\map \liminf {f \circ N} }^{\preceq_2} } }$
We have:
:$\exists j \in D: y = \map \inf {N \sqbrk {\map \precsim j} }$
By definition of reflexivity:
:$y \preceq_1 y$
Then:
:$y \in f^{-1} \sqbrk {\relcomp T {\paren {\map \liminf {f \circ N} }^{\preceq_2} } }$
Define $y' := \map \inf {\paren {f \circ N} \sqbrk {\map \precsim j} }$
Define $X' := \set {\map \inf {\paren {f \circ N} \sqbrk {\map \precsim j} }: j \in D}$
By Mapping is Increasing implies Mapping at Infimum for Sequence Precedes Infimum for Composition of Mapping and Sequence:
:$\map f y \preceq_2 y'$
By definition of $X'$:
:$y' \in X'$
By definitions of supremum and upper bound:
:$y' \preceq_2 \sup X'$
By definition of limit inferior:
:$\map \liminf {f \circ N} = \sup X'$
By definition of transitivity:
:$\map f y \preceq_2 \map \liminf {f \circ N}$
By definition of lower closure of element:
:$\map f y \in \paren {\map \liminf {f \circ N} }^{\preceq_2}$
By definition of preimage of set:
:$y \in f^{-1} \sqbrk {\paren {\map \liminf {f \circ N} }^{\preceq_2} }$
By Complement of Preimage equals Preimage of Complement:
:$f^{-1} \sqbrk {\relcomp T {\paren {\map \liminf {f \circ N} }^{\preceq_2} } } = \relcomp S {f^{-1} \sqbrk {\paren {\map \liminf {f \circ N} }^{\preceq_2} } }$
Thus this contradicts $y \in \relcomp S {f^{-1} \sqbrk {\paren {\map \liminf {f \circ N} }^{\preceq_2} } }$
{{qed|lemma}}