All charts compatible with a smooth atlas form a smooth atlas

Every chart of $\mathcal{A}$ is compatible with itself by [F3] and with [given, F2, F3] every other chart of $\mathcal{A}$ by the pairwise condition in [F2], so every chart of $\mathcal{A}$ is compatible with every chart of $\mathcal{A}$; hence $\mathcal{A}\subseteq {\mathcal{A}}^{\mathrm{\prime }}$. Since the domains of $\mathcal{A}$ cover $M$ by [F2], the domains of ${\mathcal{A}}^{\mathrm{\prime }}$ cover $M$.

Let $(U,\phi )$ and $(V,\psi )$ be charts compatible with every chart of [given, F1, F2, L1, choose] $\mathcal{A}$, and let $p\in U\cap V$. Because $\mathcal{A}$ covers $M$ by [F2], choose $(W,\chi )\in \mathcal{A}$ with $p\in W$. On $\phi (U\cap V\cap W)$ the transition factors as $\psi \circ {\phi }^{-1}=(\psi \circ {\chi }^{-1})\circ (\chi \circ {\phi }^{-1})$; the two factors are smooth because $(U,\phi )$ and $(V,\psi )$ are each compatible with $(W,\chi )$, whose overlaps with both are nonempty, so the nonempty-overlap clause of [F1] supplies all four transitions, and [L1] makes the composite smooth on $\phi (U\cap V\cap W)$.

Every point of $\phi (U\cap V)$ lies in such a set [given, F1, step 1.2] $\phi (U\cap V\cap W)$, and a map between Euclidean open sets that is smooth on an open neighbourhood of every point is smooth: the iterated coordinate partial derivatives exist and are continuous near every point, hence on all of the open set $\phi (U\cap V)$. Therefore $\psi \circ {\phi }^{-1}$ is smooth on $\phi (U\cap V)$. Interchanging the roles of $(U,\phi )$ and $(V,\psi )$ runs the same argument for $\phi \circ {\psi }^{-1}$, again through the two-sided clause of [F1].

By step 2.1 any two members of ${\mathcal{A}}^{\mathrm{\prime }}$ are smoothly compatible, and step 1.1 gives the covering condition. Hence ${\mathcal{A}}^{\mathrm{\prime }}$ is a smooth atlas by [F2]; each member of ${\mathcal{A}}^{\mathrm{\prime }}$ is compatible with every chart of $\mathcal{A}$ by the way ${\mathcal{A}}^{\mathrm{\prime }}$ was defined.