Partitions of a Closed Interval, the Set of Partitions, and Refinements

In the setting of The Real Line: Standing Notation and Background for Calculus on Intervals, let $a,b\in\mathbb{R}$ with $a<b$, let $[a,b]$ be the closed interval, and let finite sets be as in Finite Sets (i).

(i) A partition of $[a,b]$ is a finite set $P$ with $P\subseteq[a,b]$, $a\in P$ and $b\in P$.

(ii) The set of partitions of $[a,b]$ is

$$\Pi_{a,b}=\{P\in\mathcal{P}([a,b]):P\text{ is finite},\ a\in P\text{ and }b\in P\},$$

the subset of the power set $\mathcal{P}([a,b])$ given by a predicative condition (Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (ii)), a set by Sets and Maps: Ordinary Notation (iii). As the elements of $\mathcal{P}([a,b])$ are the subsets of $[a,b]$, for every set $P$: $P\in\Pi_{a,b}$ if and only if $P$ is a partition of $[a,b]$.

(iii) For partitions $P$ and $Q$ of $[a,b]$, $Q$ is a refinement of $P$, or $Q$ refines $P$, if $P\subseteq Q$.