Writing the proof by bisection

Write out the complete proof of the Bolzano-Weierstrass theorem by bisection: construct the nested intervals, stating the induction invariant, define the extraction map $\varphi$ and justify that it is strictly increasing, then conclude with the squeeze theorem.