Each smooth atlas is contained in a unique maximal smooth atlas

By [F2] and [L1], $[\mathcal{A}]$ is a smooth atlas on $M$ containing $\mathcal{A}$.

If $\mathcal{C}$ is any smooth atlas containing $\mathcal{A}$, then every [given, F1, F2] chart of $\mathcal{C}$ is compatible with every chart of $\mathcal{A}$, because all members of the single atlas $\mathcal{C}$ are pairwise compatible by [F1]; hence $\mathcal{C}\subseteq [\mathcal{A}]$ by the defining membership condition in [F2]. Applied to an atlas containing $[\mathcal{A}]$, this yields $\mathcal{C}\subseteq [\mathcal{A}]$, so $[\mathcal{A}]$ is maximal.

If $[\mathcal{A}]=[\mathcal{B}]$, then every chart of $\mathcal{A}\cup \mathcal{B}$ [given, F1, F2] belongs to the smooth atlas $[\mathcal{A}]$; therefore the domains cover $M$ and all members are pairwise compatible by [F1], so $\mathcal{A}\cup \mathcal{B}$ is a smooth atlas.

If $\mathcal{A}\cup \mathcal{B}$ is a smooth atlas, then each chart of [given, F1, F2, step 1.2] $\mathcal{B}$ is compatible with every chart of $\mathcal{A}$, so $\mathcal{B}\subseteq [\mathcal{A}]$ by [F2]; symmetrically $\mathcal{A}\subseteq [\mathcal{B}]$. Step 1.2 applied to the atlas $[\mathcal{B}]$ containing $\mathcal{B}$ gives $[\mathcal{B}]\subseteq [\mathcal{A}]$, and the same argument with $A$ and $B$ exchanged gives $[\mathcal{A}]\subseteq [\mathcal{B}]$. Hence $[\mathcal{A}]=[\mathcal{B}]$.

Steps 1.1 and 1.2 prove that $[\mathcal{A}]$ is a maximal smooth atlas [step 1.1, step 1.2, step 2.1] containing $\mathcal{A}$. If $\mathcal{C}$ is any maximal smooth atlas containing $\mathcal{A}$, then step 1.2 gives $\mathcal{C}\subseteq [\mathcal{A}]$, and this containment cannot be proper because $[\mathcal{A}]$ is itself a smooth atlas by step 1.1. Therefore $\mathcal{C}=[\mathcal{A}]$, and with steps 1.3 and 2.1 all three claims are proved.