上确界性质与连续函数有界性的等价性

嘿，这个问题真的值得琢磨！在微积分课程里，我们证明的好多定理，本质上都是实数集$\mathbb{R}$的上确界性质的直接推论。比如介值定理、波尔查诺-魏尔斯特拉斯定理，后来发现它们其实和上确界性质是等价的——你用其中一个就能推出另一个。

那我现在想问的是：「闭区间上的连续函数一定在该区间上有界」这个结论，是不是也和上确界性质等价？

换句话说：如果有一个有序域$F$，满足“所有在闭区间上连续的函数都在该区间上有界”，那$F$是不是一个完备的有序域（也就是满足上确界性质）？

我们知道，从极值定理出发，很容易证明罗尔定理，接着就能推出中值定理，而通过中值定理可以反推得到上确界性质。但我现在问的是更基础的情况——我们只假设闭区间上的连续函数有界，不额外假设它们能取到最大值，这种情况下还能推出上确界性质吗？

下面我会给出一个（篇幅不算短的）证明，如果我们...

备注：内容来源于stack exchange，提问作者Or Aviram