[proofplan] We show that adding a single point to a partition can only decrease the upper sum and increase the lower sum, because restricting the supremum (resp. infimum) to a smaller subinterval cannot increase (resp. decrease) it. A general refinement is obtained by adding points one at a time and applying this single-point result inductively. [/proofplan] [step:Prove the single-point refinement inequality] Let $\mathcal{D} = \{x_0, x_1, \ldots, x_n\}$ be a partition of $[a,b]$, and suppose $\mathcal{D}' = \mathcal{D} \cup \{y\}$ where $y \in (x_{r-1}, x_r)$ for some index $r$. Define $M_r = \sup_{[x_{r-1}, x_r]} f$. Since $[x_{r-1}, y] \subseteq [x_{r-1}, x_r]$ and $[y, x_r] \subseteq [x_{r-1}, x_r]$, we have \begin{align*} \sup_{[x_{r-1}, y]} f \le M_r \qquad \text{and} \qquad \sup_{[y, x_r]} f \le M_r. \end{align*} Therefore \begin{align*} \sup_{[x_{r-1}, y]} f \cdot (y - x_{r-1}) + \sup_{[y, x_r]} f \cdot (x_r - y) &\le M_r(y - x_{r-1}) + M_r(x_r - y) \\ &= M_r(x_r - x_{r-1}). \end{align*} All subintervals other than $[x_{r-1}, x_r]$ are unchanged by the refinement, so summing over all subintervals gives $S(f, \mathcal{D}') \le S(f, \mathcal{D})$. [guided] The same argument works for lower sums with reversed inequalities. Define $m_r = \inf_{[x_{r-1}, x_r]} f$. Since $[x_{r-1}, y] \subseteq [x_{r-1}, x_r]$, we have $\inf_{[x_{r-1}, y]} f \ge m_r$ (restricting to a subset can only raise the infimum). Similarly $\inf_{[y, x_r]} f \ge m_r$. Therefore \begin{align*} \inf_{[x_{r-1}, y]} f \cdot (y - x_{r-1}) + \inf_{[y, x_r]} f \cdot (x_r - y) &\ge m_r(y - x_{r-1}) + m_r(x_r - y) \\ &= m_r(x_r - x_{r-1}). \end{align*} Summing over all subintervals gives $s(f, \mathcal{D}') \ge s(f, \mathcal{D})$. The geometric intuition is that splitting a subinterval allows the supremum (resp. infimum) on each piece to better approximate $f$, tightening the upper sum downward and the lower sum upward. [/guided] [/step] [step:Extend to a general refinement by induction on the number of added points] Any refinement $\mathcal{D}'$ of $\mathcal{D}$ is obtained by adding finitely many points $y_1, y_2, \ldots, y_m$ to $\mathcal{D}$. Define $\mathcal{D}_0 = \mathcal{D}$ and $\mathcal{D}_j = \mathcal{D}_{j-1} \cup \{y_j\}$ for $j = 1, \ldots, m$, so that $\mathcal{D}_m = \mathcal{D}'$. Applying the single-point result from the previous step at each stage: \begin{align*} S(f, \mathcal{D}) = S(f, \mathcal{D}_0) \ge S(f, \mathcal{D}_1) \ge \cdots \ge S(f, \mathcal{D}_m) = S(f, \mathcal{D}'). \end{align*} Similarly: \begin{align*} s(f, \mathcal{D}) = s(f, \mathcal{D}_0) \le s(f, \mathcal{D}_1) \le \cdots \le s(f, \mathcal{D}_m) = s(f, \mathcal{D}'). \end{align*} Combining with the standing inequality $S(f, \mathcal{D}') \ge s(f, \mathcal{D}')$ (which holds for any partition, since $\sup \ge \inf$ on every subinterval) yields the full chain: \begin{align*} S(f, \mathcal{D}) \ge S(f, \mathcal{D}') \ge s(f, \mathcal{D}') \ge s(f, \mathcal{D}). \end{align*} [/step]