Proving the nested interval theorem 
Theorem:
Let $\{I_n\}_{n \in \mathbb N}$ be a collection of closed intervals with the following properties:

*

*$I_n$ is closed $\forall \,n$, say $I_n = [a_n,b_n]$;

*$I_{n+1} \subseteq I_n$$\forall \,n$.
Then $\displaystyle\bigcap_{n=1}^{\infty} I_n \ne \emptyset$.


Pf: Let $I_n $ be intervals that satisfy 1 and 2. Say $I_n = [a_n, b_n] \forall n\ge 1$.
Let the sets $A$ and $B$ be defined by $A = \{a_n\}$ and $B = \{b_n\}$.
Therefore $\forall n,k \ge 1$, $a_k \le b_n$.
Case 1: $k \le n$
Then $[a_n,b_n] \subset [a_k, b_k]$ therefore $b_n \in [a_k,b_k]$ and $a_k \le b_n \le b_k$ therefore $a_k \le b_k$.
Case 2: $k>n$
Therefore $I_k \subset I_n$. By nestedness, $[a_k,b_k] \subset [a_n,b_n]$, therefore $a_k \le b_n$.
Claim: $\sup A \le \inf B$.
Proof of claim: Let $A$ and $B$ be sets such that for all $a \in A$ and for all $b \in B$, $a \le b$ Therefore $\sup A \le b$ and $a \le \inf B$ therefore $\sup A \le \inf B$.
Now we must prove that either $\bigcap_{n=1}^{\infty} I_n = [\sup A, \inf B]$ or $\bigcap_{n=1}^{\infty} I_n = \emptyset$.
First we will show $[\sup A, \inf B] \subset \bigcap I_n$. Let $x \in [\sup A, \inf B]$. Therefore $\sup A \le x \le \inf B$ and $\forall n $, $a_n \le \sup A \le x \le \inf B \le b_n$ or $a_n \le x \le b_n$ and thus $x \in I_n$.
Now we will show that $\bigcap I_n \subset [\sup A, \inf B]$. Let $y \in \bigcap I_n$. Show $\sup A \le y \le \inf B$. We know that $\forall n \ge 1$, $a_n \le y \le b_n$. Since $a_n \le y$, we see that $\sup A \le y$.
Similarly since $y \le b_n$, we see that $y \le \inf B$.

As you can see, this proof is very long. Does anyone have any advice to shorten this?

 A: Here is a non-constructive proof.
Construct a sequence by choosing an element $x_n \in I_n$ for every $n$; you can do this however you like. Since this sequence is bounded then the Bolzano-Weierstrass theorem says there exists a convergent subsequence $x_{n_k}$ converging to some real number $c$. Suppose $c \not\in \bigcap_{n=1}^{\infty} I_n$. Then there exists some $N$ for which $c \not\in I_n$ for all $n > N$, and so there is some number $\varepsilon >0$ such that $|x_{n_k} - c| \geq \varepsilon$ for all $n_k > N$ contradicting convergence. Thus $c \in \bigcap_{n=1}^{\infty} I_n$ and so it is nonempty.
A: As $I_{n+1} \subset I_n$, it follows that any $a_m$ is a lower bound for $\left\{b_n\right\}$ and vice-versa for any $b_m$ being an upper bound for $\left\{a_n\right\}$. $\left\{a_n\right\}$, $\left\{b_n\right\}$ are non-empty so $a= \sup\left\{a_n\right\}$, $b= \inf\left\{b_n\right\}$ exist.
Further, $a\leq b$, as if $b < a$ we can find $a_n, b_m$ arbitrarily close to $a,b$ respectfully, so it would be possible to find $b_m < a_n$ which would be a contradiction. So $[a,b]$ is well defined and $a_n \le a, b \le b_n$ $\forall n$ so $[a,b] \subset I_n$ $\forall n$. So $[a,b] \subset \bigcap_n I_n$.
A: Well, I didn't see the reason to introduce the extra subscript $k$.

Let $a=\sup\{a_n\}$ and $b=\inf\{b_n\}$, where the existence of $a$ and $b$ follows from the boundedness of $I_1$. If $a<b$, then $[a,b]\subseteq \cap_{n\in \mathbb N} I_n$ and we are done.
Suppose not, i.e. $a>b$. We may find large $n$ such that $a_n$ and $b_n$ are close to $a$ and $b$, respectively, which implies $a_n>b_n$. A contradiction.
$\tag*{$\square$}$
