I'm working on proving the following:
Lemma: Let $I$ be a bounded interval, and let P and P' be two partitions of $I$. Then the common refinement of P and P', P#P' is also a partition of I, and is both finer than P and finer than P'.
where a partition P of a bounded set $I$ is defined as a finite set of bounded intervals contained in $I$ such that $x\in I \Rightarrow \exists ! J\in\ $P such that $x\in J$; P' is finer that P if $\forall J\in\ $P' $\exists K\in $P such that $J\subseteq K$ and finally P#P'$:=\{K\cap J:K\in$P and $J\in $ P'$\}$.
Now, I've proved that:
(1) every element in P#P' is a bounded interval contained in $I$;
(2) $x\in I \Rightarrow \exists ! H\in\ $P#P' such that $x\in H$;
(3) P#P' is finer than both P and P';
the only thing that is left is to show that P#P' is finite.
To do this I thought about showing that the cardinality of P#P' $\leq$ cardinality of P $\times$ cardinality of P' by first finding a bijection between each $K\cap J \in $P#P' and each ordered pair $(K,J)\in $P$\times$P'. But this approach seems too intricate to me to prove such a result so I'd like to know if anyone knows of a simpler way to prove this.
EDIT: Do you think the following proof is rigorous enough?
Let $M$ be the cardinality of P and $N$ the cardinality of P'; then, since for each $K\in $P there are at most $N$ intervals $J\in $P' such that $K\cap J\in $P#P' we have that for each $K\in $P there are at most $N$ elements in P#P'. Now, since the elements $K\in $P are themselves at most $M$ it follows that P#P' has at most $M\cdot N$ elements and is thus finite.
The function $\boldsymbol{P}\times\boldsymbol{P'}\to\boldsymbol{P}$#$\boldsymbol{P'}$ prescribed by$\langle K,J\rangle\mapsto K\cap J$ is evidently surjective.
This allows us to conclude that the cardinality of $\boldsymbol{P}$#$\boldsymbol{P'}$ will not exceed the cardinality of $\boldsymbol{P}\times\boldsymbol{P'}$, hence will be finite.