Generalizations of the Heine-Borel theorem to more general LOTS A couple of us over at ProofWiki believe we've proven, at http://proofwiki.org/wiki/Compact_Subspace_of_Linearly_Ordered_Space , that if $X$ is a linearly ordered topological space and $Y \subseteq X$, then $Y$ is compact iff for each nonempty $S \subseteq Y$:


*

*$S$ has a supremum and infimum in $X$ and

*$\sup S, \inf S \in Y$.
First off, I'd love to know if we've made some error. Second off, I wasn't able to come up with a proof of the reverse implication in pure ZF—the technique we used requires the ultrafilter lemma. Is there some way to avoid it?
Similarly, it appears that a consequence of this theorem is that a linearly ordered topological space is Dedekind complete iff its compact subsets are precisely its closed and bounded subsets. Is there a way to prove that without UL?
 A: All interval notation is taken in $Y$ unless subscripted with an $X$. E.g., $[a,\to)=\{y\in Y:a\le y\}$, while $[a,\to)_X=\{x\in X:a\le x\}$.
Let $\mathscr{U}$ be an open cover of $Y$. Without loss of generality we may assume that each $U\in\mathscr{U}$ is order-convex. Define a relation $\sim$ on $\mathscr{U}$ by $U\sim V$ iff there is a finite family $\{U_0,\dots,U_n\}\subseteq\mathscr{U}$ such that $U=U_0$, $V=U_n$, and $U_k\cap U_{k+1}\ne\varnothing$ for $k=0,\dots,n-1$; it’s easy to check that $\sim$ is an equivalence relation on $\mathscr{U}$. For $U\in\mathscr{U}$ let $[U]$ be the $\sim$-class of $U$. Then $\mathscr{C}=\left\{\bigcup[U]:U\in\mathscr{U}\right\}$ is a partition of $Y$ into order-convex open sets, so each $[U]$ is in fact clopen. Note that since its elements are order-convex, $\mathscr{C}$ inherits a natural linear order from $Y$, which I will also denote by $\le$.
It’s not hard to show that (1) and (2) imply that $\inf C,\sup C\in C$ for each $C\in\mathscr{C}$; let $a_C=\inf C$ and $b_C=\sup C$, so that $C=[a_C,b_C]$. Let $C\in\mathscr{C}$, and suppose that $a_C\ne\inf Y$. Since $[a_C,\to)$ is open in $Y$ there is an $x\in X$ such that $x<a_C$ and for all $y\in(\leftarrow,a_C)$ we have $y\le x$. Let $u=\sup\big(Y\cap(\leftarrow,x)_X\big)$; then $u\in Y$, so $u=b_D$ for some $D\in\mathscr{C}$. Clearly $D$ is the immediate predecessor of $C$ in $\mathscr{C}$. A similar argument shows that if $b_C\ne\sup Y$, then $C$ has an immediate successor in $\mathscr{C}$.
Fix $C_0\in\mathscr{C}$. Given $C_n\in\mathscr{C}$ for some $n\in\Bbb N$, either $C_n$ is the maximum element of $\mathscr{C}$, in which case the construction stops, or $C_n$ has an immediate successor in $\mathscr{C}$, and we define $C_{n+1}$ to be that successor. Suppose that the construction does not stop at any finite stage. Let $a=\sup\{a_n:n\in\Bbb N\}$. Then $a\notin\bigcup_{n\in\Bbb N}C_n$, so $a=a_D$ for some $D\in\mathscr{C}$, and this $D$ has no immediate predecessor in $\mathscr{C}$. This is impossible, so the construction must stop at some finite stage. A similar argument working to the left shows that $\mathscr{C}$ must in fact be finite. 
Fix $C\in\mathscr{C}$. There are $U,V\in\mathscr{U}$ such that $a_C\in U$ and $b_C\in V$. Then $U,V\subseteq C$, so $U\sim V$, and there is a finite family $\{U_0,\dots,U_n\}\subseteq\mathscr{U}$ such that $U=U_0$, $V=U_n$, and $U_k\cap U_{k+1}\ne\varnothing$ for $k=0,\dots,n-1$; clearly $\{U_k:k=0,\dots,n\}$ is a finite subfamily of $\mathscr{U}$ covering $C$, and it follows that $\mathscr{U}$ has a finite subcover.
