The definition of a smooth structure is by means of a maximal atlas: an atlas of charts refines another one if it adds charts (in such a way that the overlap functions remain smooth). The existence of maximal atlases, that cannot further be refined, follows from Zorn's lemma.