Theorem: Equivalence of Definitions of Boolean Lattice/Definition 3 implies Definition 1

Let $\BB = \struct {S, \vee, \wedge, \preceq, \bot, \top}$ be a bounded lattice.
Let $\neg$ be a unary operation on $S$ such that:
:$\paren 1 \quad \forall a, b \in S: a \preceq \neg b \iff a \wedge b = \bot$
:$\paren 2 \quad \forall a \in S: \neg \neg a = a$
Then, $\BB$ is complemented and distributive.

Proof:
Let us begin with some identities.
First:
:$\paren R \quad a \preceq \neg b \iff b \preceq \neg a$
since both are equivalent to $a \wedge b = \bot$ by $\paren 1$.
Second:
:$\paren M \quad a \preceq \neg \paren {\neg a \wedge b}$
which follows by $\paren R$ from:
:$\neg a \wedge b \preceq \neg a$
because Meet Precedes Operands.
Third:
:$\paren J \quad \neg \paren {c \vee d} \preceq \neg c$
derived from $\paren M$ by substituting $\neg \paren {c \vee d}$ for $a$ and $c$ for $b$, then applying $\paren 2$ and Meet Absorbs Join.
Now, we will obtain our first significant result:
:$\paren D \quad \neg a \wedge \neg b = \neg \paren {a \vee b}$
Since by $\paren M$ we have:
:$a \preceq \neg \paren {\neg a \wedge \neg b}$
:$b \preceq \neg \paren {\neg a \wedge \neg b}$
then by definition of join:
:$a \vee b \preceq \neg \paren {\neg a \wedge \neg b}$
so applying $\paren R$ gives:
:$\neg a \wedge \neg b \preceq \neg \paren {a \vee b}$
Also, by $\paren J$:
:$\neg \paren {a \vee b} \preceq \neg a$
:$\neg \paren {a \vee b} \preceq \neg b$
and so by definition of meet:
:$\neg \paren {a \vee b} \preceq \neg a \wedge \neg b$
Hence, $\paren D$ follows by antisymmetry.
Next, we can show that:
:$\paren A \quad \neg a \wedge \paren {a \vee b} = \neg a \wedge b$
By Join Succeeds Operands and Meet is Increasing:
:$\neg a \wedge b \preceq \neg a \wedge \paren {a \vee b}$
By Meet Precedes Operands:
:$\neg a \wedge \paren {a \vee b} \preceq \neg a$
and since by $\paren C$:
:$\bot = \paren {a \vee b} \wedge \neg \paren {a \vee b} = \paren {a \vee b} \wedge \neg a \wedge \neg b$
it follows from $\paren 1$ that:
:$\neg a \wedge \paren {a \vee b} \preceq b$
So, $\paren A$ follows by definition of meet and antisymmetry.
Lastly, we also will need the dual of $\paren A$:
:$\paren {A'} \quad \neg a \vee \paren {a \wedge b} = \neg a \vee b$
which can be derived from $\paren A$ by use of $\paren D$ and $\paren 2$.
=== Complemented ===
Since $\neg a \preceq \neg a$, we have by $\paren 1$ that:
:$\neg a \wedge a = \bot$
Rewriting $a$ as $\neg \neg a$ by $\paren 2$, and applying $\paren D$, we find:
:$\neg \paren {a \vee \neg a} = \bot$
and so by $\paren 2$:
:$a \vee \neg a = \neg \bot$
But for any $b \in S$:
:$\bot \preceq \neg b$
so by $\paren R$:
:$b \preceq \neg \bot$
Thus:
:$\neg \bot = \top$
by definition.
Therefore, $\neg a$ is a complement of $a$ for every $a \in S$.
{{qed|lemma}}
=== Distributive ===
From Join of Meets Precedes Meet with Join:
:$\paren {x \wedge y} \vee \paren {x \wedge z} \preceq x \wedge \paren {y \vee z}$
Before we prove the other direction of inequality, we need one more fact:
{{begin-eqn}}
{{eqn | l = \neg a \wedge \paren {a \vee b}
      | r = \neg a \wedge b
      | c = $\paren A$
}}
{{eqn | o = \preceq
      | r = b
}}
{{eqn | ll = \leadsto
      | l = x \wedge \paren {\neg x \vee y \vee \paren {x \wedge z} }
      | o = \preceq
      | r = y \vee \paren {x \wedge z}
      | c = Substitute $a = \neg x$ and $b = y \vee \paren {x \wedge z}$, and apply $\paren 2$
}}
{{eqn | ll = \leadsto
      | l = x \wedge \paren {\neg x \vee y \vee z}
      | o = \preceq
      | r = y \vee \paren {x \wedge z}
      | c = $\paren {A'}$
}}
{{eqn | ll = \leadsto
      | l = x \wedge \paren {y \vee z}
      | o = \preceq
      | r = y \vee \paren {x \wedge z}
      | c = $\paren 2$ and $\paren A$
}}
{{end-eqn}}
Now, we can complete the proof.
In addition to the above fact, we have by Meet Precedes Operands:
:$x \wedge \paren {y \vee z} \preceq x$
and so by definition of join:
:$x \wedge \paren {y \vee z} \preceq x \wedge \paren {y \vee \paren {x \wedge z}}$
By the fact once more, substituting $x = x'$, $y = x' \wedge z'$, $z = y'$, we obtain:
:$x' \wedge \paren {\paren {x' \wedge z'} \vee y'} \preceq \paren {x' \wedge z'} \vee \paren {x' \wedge y'}$
So by transitivity after renaming the variables:
:$x \wedge \paren {y \vee z} \preceq \paren {x \wedge y} \vee \paren {x \wedge z}$
Hence the result by antisymmetry.
{{qed}}