Proof of Theorem 2.7, p. 14 — a maximal commutative ∗-subalgebra contains every element of $\mathcal A$ commuting with it

Let $\mathcal A \subseteq \mathbb C^{n\times n}$ be a matrix ∗-algebra and let $\mathcal B \subseteq \mathcal A$ be an inclusionwise maximal commutative ∗-subalgebra of $\mathcal A$. Then every $X \in \mathcal A$ that commutes with every element of $\mathcal B$ is itself an element of $\mathcal B$:

This is the first step of the paper's elementary proof of Theorem 2.7: the relative commutant of $\mathcal B$ in $\mathcal A$ is $\mathcal B$ itself, which later forces the diagonal blocks of every element of $\mathcal A$ to be scalar.

Formalization Note Matrix ∗-algebras are NonUnitalStarSubalgebras (no unit assumed); maximality is among commutative NonUnitalStarSubalgebras between $\mathcal B$ and $\mathcal A$.