The diagram
commutes, i.e. we have
\[ \mathsf{I}_{*}\webleft (\mathsf{I}\webleft (U\webright )\webright )=[\mspace {-3mu}[x\mapsto [\mspace {-3mu}[y\mapsto U]\mspace {-3mu}]]\mspace {-3mu}] \]
for each $U\in \mathcal{P}\webleft (X\webright )$.
We have
\begin{align*} \mathsf{I}_{*}\webleft (\mathsf{I}\webleft (U\webright )\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathsf{I}_{*}\webleft ([\mspace {-3mu}[x\mapsto U^{\textsf{c}}\cup \webleft\{ x\webright\} ]\mspace {-3mu}]\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[\mspace {-3mu}[x\mapsto \mathsf{I}\webleft (U^{\textsf{c}}\cup \webleft\{ x\webright\} \webright )]\mspace {-3mu}]\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[\mspace {-3mu}[x\mapsto [\mspace {-3mu}[y\mapsto \webleft (U^{\textsf{c}}\cup \webleft\{ x\webright\} \webright )^{\textsf{c}}\cup \webleft\{ x\webright\} ]\mspace {-3mu}]]\mspace {-3mu}]\\ & = [\mspace {-3mu}[x\mapsto [\mspace {-3mu}[y\mapsto \webleft (U\cap \webleft (X\setminus \webleft\{ x\webright\} \webright )\webright )\cup \webleft\{ x\webright\} ]\mspace {-3mu}]]\mspace {-3mu}]\\ & = [\mspace {-3mu}[x\mapsto [\mspace {-3mu}[y\mapsto \webleft (U\setminus \webleft\{ x\webright\} \webright )\cup \webleft\{ x\webright\} ]\mspace {-3mu}]]\mspace {-3mu}]\\ & = [\mspace {-3mu}[x\mapsto [\mspace {-3mu}[y\mapsto U]\mspace {-3mu}]]\mspace {-3mu}], \end{align*}
where we have used Item 2 of Proposition 2.3.11.1.2 for the fourth equality above.
