So, as the title suggests, there's point about the proof of the Tychonoff theorem I don't quite get. The theorem in Munkres is based on the "closed set and finite intersection" formulation of compactness, which, after doing some google-ing, I found out to be a less formal version of the Cartan-Bourbaki proof, based on filter theory, which I don't yet know anything about. However, the proof in Munkres doesn't invoke the concept of filters explicitly, so I find it rather accessible at this stage. Before the proof itself two lemmas are presented, and the way one of them is laid out confuses me a bit. I'll quote the directly, for convenience. Lemma 37.1. Let X be a set, let A be a collection of subsets of X having the finite intersection property. Then there exists a collection D of subsets of X such that D contains A, and D has the finite intersection property, and no collection of subsets of X that properly contains D has this property. Lemma 37.2. Let X be a set, let D be a collection of subsets of X that is maximal with respect to the finite intersection property. Then: (a) Any finite intersection of elements of D is an element of D. (b) If A is a subset of X that intersects every element of D, then A is an element of D. Now, what I don't understant is this: In Lemma 37.1., Zorn's lemma is invoked in order to prove the existence of the collection D, by means of taking a specific collection A with a strict partial order (I won't go into detail), and proving that every subcollection B of A (referred to as "subsuperset" in the proof) has an upper bound in A. From that it follows that A as a maximal element D. But, I don't understand why it's stated in the Lemma that D has the finite intersection property, when this fact is proved in Lemma 37.2.? In the lemma only existence of D is proved, as far as I understand. Thanks in advance for any replies.