Auxiliary Approximating Relation has Interpolation Property

== Theorem ==
Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $x, z \in S$ such that:
:$x \ll z \land x \ne z$
Let $\RR$ be an auxiliary approximating relation on $S$.
Then
:$\exists y \in S: \tuple {x, y} \in \RR \land \tuple {y, z} \in \RR \land x \ne y$
== Proof ==
Define $I := \set {u \in S: \exists y \in S: \tuple {u, y} \in \RR \land \tuple {y, z} \in \RR}$
By definition of auxiliary relation:
:$\tuple {\bot, \bot} \in \RR$ and $\tuple {\bot, z} \in \RR$
where $\bot$ denotes the smallest element in $L$.
Then
:$\bot \in I$
By definition:
:$I$ is a non-empty set.
We will prove that
:$I$ is a lower section.
Let $a \in I, b \in S$ such that
:$b \preceq a$
By definition of $I$:
:$\exists s \in S: \tuple {a, s} \in \RR \land \tuple {s, z} \in \RR$
By definitions of auxiliary relation and reflexivity:
:$\tuple {b, s} \in \RR$
Thus
:$b \in I$
We will prove that
:$I$ is directed.
Let $a, b \in I$.
By definition of $I$:
:$\exists s \in S: \tuple {a, s} \in \RR \land \tuple {s, z} \in \RR$
and
:$\exists t \in S: \tuple {b, t} \in \RR \land \tuple {t, z} \in \RR$
By Auxiliary Relation is Congruent:
:$\tuple {a \vee b, s \vee t} \in \RR$
By definition of auxiliary relation:
:$\tuple {s \vee t, z} \in \RR$
Thus by definition of $I$:
:$a \vee b \in I$
Thus by Join Succeeds Operands:
:$a \preceq a \vee b$ and $b \preceq a \vee b$
By definition:
:$I$ is ideal in $L$.
We will prove that
:$I \subseteq z^{\RR}$
Let $a \in I$.
By definition of $I$:
:$\exists s \in S: \tuple {a, s} \in \RR \land \tuple {s, z} \in \RR$
By definition of auxiliary relation:
:$a \preceq s$
Again by definition of auxiliary relation and reflexivity:
:$\tuple {a, z} \in \RR$
Thus by definition of $\RR$-segment:
:$a \in z^{\RR}$
By Supremum of Subset and definition of approximating relation:
:$\sup I \preceq \sup \left({z^{\RR} }\right) = z$
We will prove that
:$\sup I = z$
:$\sup I \ne z$
By definition of $\prec$:
:$\sup I \prec z$
Then by definition of antisymmetry:
:$z \npreceq \sup I$
By Not Preceding implies Approximating Relation and not Preceding:
:$\exists y \in S: \tuple {y, z} \in \RR \land y \npreceq \sup I$
Again by Not Preceding implies Approximating Relation and not Preceding:
:$\exists u \in S: \tuple {u, y} \in \RR \land u \npreceq \sup I$
By definition of $I$:
:$u \in I$
This contradicts $u \preceq \sup I$ by definition of supremum.
By Way Below iff Second Operand Preceding Supremum of Ideal implies First Operand is Element of Ideal:
:$x \in I$
By definition of $I$:
:$\exists s \in S: \tuple {x, s} \in \RR \land \tuple {s, z} \in \RR$
By definition of auxiliary relation:
:$x \preceq s$
By definition of auxiliary relation and reflexivity:
:$\tuple {x, z} \in \RR$
By Auxiliary Approximating Relation has Quasi Interpolation Property:
:$\exists y \in S: x \preceq y \land \tuple {y, z} \in \RR \land x \ne y$
By definition of $\prec$:
:$ x \prec y$
Define $Y := s \vee y$
By Join Succeeds Operands:
:$s \preceq Y$ and $y \preceq Y$
Then 
:$x \ne Y$
By definition of reflexivity:
:$x \preceq x$
By definition of auxiliary relation:
:$\tuple {x, Y} \in \RR$
Again by definition of auxiliary relation:
:$\tuple {Y, z} \in \RR$
Hence
:$\exists y \in S: \tuple {x, y} \in \RR \land \tuple {y, z} \in \RR \land x \ne y$
== Sources ==
* 
* 
Category:Approximating Relations
Category:Complete Lattices
Category:Auxiliary Relations