User:Dfeuer/Order Completion is Minimal

Note: our current definition of completion is as a superset. We presumably want also a definition as an order embedding. This theorem will of course take on a slightly different form in that case.

Theorem

Let $\struct {T, \le}$ be a complete lattice.

Let $S \subseteq T$.

Suppose that $T$ is an order completion of $S$.

Then for any $U$ such that $S \subseteq U \subsetneqq T$,

$\struct {U, \le}$ is not complete.

Proof

Aiming for a contradiction, suppose $U$ is complete.