[proofplan] We establish three properties of the Galois correspondence $\Phi: H \mapsto K^H$. First, we show that $\Phi$ reverses inclusion: $H_1 \le H_2$ implies $K^{H_2} \subset K^{H_1}$, and conversely. Second, we prove $K^{H_1 \cap H_2} = K^{H_1} \cdot K^{H_2}$ by showing each side is contained in the other, using the [quotetheorem:1274] to translate between subgroups and fixed fields. Third, we prove $K^{\langle H_1, H_2 \rangle} = K^{H_1} \cap K^{H_2}$ by a similar double-containment argument. The key tool throughout is the bijectivity of the Galois correspondence for finite Galois extensions, which guarantees that $\operatorname{Gal}(K/K^H) = H$ for every $H \le G$ and $K^{\operatorname{Gal}(K/E)} = E$ for every intermediate field $k \subset E \subset K$. [/proofplan]

[step:Establish that the Galois correspondence reverses inclusion]Let $H_1, H_2 \le G$ with $H_1 \le H_2$. If $\alpha \in K^{H_2}$, then $\sigma(\alpha) = \alpha$ for all $\sigma \in H_2$. Since $H_1 \subset H_2$, every $\sigma \in H_1$ also satisfies $\sigma(\alpha) = \alpha$, so $\alpha \in K^{H_1}$. Therefore $K^{H_2} \subset K^{H_1}$. Conversely, suppose $K^{H_2} \subset K^{H_1}$. By the [quotetheorem:1274], the Galois correspondence is a bijection and $\operatorname{Gal}(K/K^H) = H$ for every subgroup $H \le G$. If $\sigma \in H_1$, then $\sigma$ fixes $K^{H_1}$ pointwise. Since $K^{H_2} \subset K^{H_1}$, the field $K^{H_1}$ is contained in $K^{H_2}$ — but we assumed the reverse inclusion $K^{H_2} \subset K^{H_1}$. From $K^{H_2} \subset K^{H_1}$, every element fixed by $H_2$ is also fixed by $H_1$, but this does not directly give $H_1 \le H_2$. We use the contrapositive through the Galois correspondence: since $H \mapsto K^H$ is inclusion-reversing (just proved) and $K^H \mapsto \operatorname{Gal}(K/K^H) = H$ is also inclusion-reversing (more automorphisms fix a smaller field), the composition is inclusion-preserving and is the identity on subgroups. Thus $K^{H_2} \subset K^{H_1}$ implies $H_1 = \operatorname{Gal}(K/K^{H_1}) \le \operatorname{Gal}(K/K^{H_2}) = H_2$. Therefore $\Phi$ is an order-reversing bijection between the lattice of subgroups of $G$ and the lattice of intermediate fields of $K/k$.[/step]

[guided]We verify that the map $\Phi: H \mapsto K^H$ reverses the inclusion order. **Forward direction: $H_1 \le H_2 \implies K^{H_2} \subset K^{H_1}$.** Let $H_1, H_2 \le G$ with $H_1 \le H_2$. Take any $\alpha \in K^{H_2}$. Then $\sigma(\alpha) = \alpha$ for all $\sigma \in H_2$. Since $H_1 \subset H_2$, every $\sigma \in H_1$ is also in $H_2$, so $\sigma(\alpha) = \alpha$. Therefore $\alpha \in K^{H_1}$, giving $K^{H_2} \subset K^{H_1}$. The intuition is that more automorphisms impose more constraints on fixed elements, so the fixed field shrinks. **Converse: $K^{H_2} \subset K^{H_1} \implies H_1 \le H_2$.** The [quotetheorem:1274] provides the inverse map $\Psi: E \mapsto \operatorname{Gal}(K/E)$ with the property that $\Psi \circ \Phi = \operatorname{id}$ on subgroups (i.e., $\operatorname{Gal}(K/K^H) = H$ for every $H \le G$). The map $\Psi$ is also order-reversing: if $E_1 \subset E_2$, then any automorphism fixing $E_2$ pointwise also fixes $E_1$ pointwise (since $E_1 \subset E_2$), so $\operatorname{Gal}(K/E_2) \le \operatorname{Gal}(K/E_1)$. Applying $\Psi$ to the inclusion $K^{H_2} \subset K^{H_1}$ gives \begin{align*} H_1 = \operatorname{Gal}(K/K^{H_1}) \le \operatorname{Gal}(K/K^{H_2}) = H_2. \end{align*} This shows the correspondence is a bijection that reverses order in both directions — an anti-isomorphism of partially ordered sets.[/guided]

[step:Prove $K^{H_1 \cap H_2} = K^{H_1} \cdot K^{H_2}$]We show the two containments separately. **Containment $K^{H_1} \cdot K^{H_2} \subset K^{H_1 \cap H_2}$:** Let $\alpha \in K^{H_1}$ and $\beta \in K^{H_2}$. For any $\sigma \in H_1 \cap H_2$, we have $\sigma \in H_1$, so $\sigma(\alpha) = \alpha$, and $\sigma \in H_2$, so $\sigma(\beta) = \beta$. Therefore $\sigma$ fixes both $\alpha$ and $\beta$, hence it fixes every element of the compositum $K^{H_1} \cdot K^{H_2}$ (since the compositum is generated as a field by elements of $K^{H_1}$ and $K^{H_2}$). This gives $K^{H_1} \cdot K^{H_2} \subset K^{H_1 \cap H_2}$. **Containment $K^{H_1 \cap H_2} \subset K^{H_1} \cdot K^{H_2}$:** By the [quotetheorem:1274], it suffices to show that $\operatorname{Gal}(K / K^{H_1} \cdot K^{H_2}) = H_1 \cap H_2$. We have already shown $\operatorname{Gal}(K / K^{H_1} \cdot K^{H_2}) \subset H_1 \cap H_2$ (any automorphism fixing the compositum fixes both $K^{H_1}$ and $K^{H_2}$, hence lies in $\operatorname{Gal}(K/K^{H_1}) \cap \operatorname{Gal}(K/K^{H_2}) = H_1 \cap H_2$). For the reverse, if $\sigma \in H_1 \cap H_2$, then $\sigma$ fixes $K^{H_1}$ and $K^{H_2}$ pointwise, hence fixes their compositum $K^{H_1} \cdot K^{H_2}$ pointwise, so $\sigma \in \operatorname{Gal}(K / K^{H_1} \cdot K^{H_2})$. Therefore $\operatorname{Gal}(K / K^{H_1} \cdot K^{H_2}) = H_1 \cap H_2$. Since the Galois correspondence is a bijection and $\operatorname{Gal}(K / K^{H_1} \cdot K^{H_2}) = H_1 \cap H_2 = \operatorname{Gal}(K / K^{H_1 \cap H_2})$, we conclude $K^{H_1} \cdot K^{H_2} = K^{H_1 \cap H_2}$.[/step]

[guided]This identity says that the meet (intersection) of two subgroups maps to the join (compositum) of the corresponding fixed fields. This is the hallmark of an anti-isomorphism of lattices: meets and joins are swapped. **Containment $K^{H_1} \cdot K^{H_2} \subset K^{H_1 \cap H_2}$:** Let $\alpha \in K^{H_1}$ and $\beta \in K^{H_2}$. For any $\sigma \in H_1 \cap H_2$, we have $\sigma \in H_1$, so $\sigma(\alpha) = \alpha$, and $\sigma \in H_2$, so $\sigma(\beta) = \beta$. Therefore $\sigma$ fixes both $\alpha$ and $\beta$, hence fixes every element of the compositum $K^{H_1} \cdot K^{H_2}$ (since the compositum is generated as a field by elements of $K^{H_1}$ and $K^{H_2}$, and any field automorphism fixing a set of generators fixes the generated field). This gives $K^{H_1} \cdot K^{H_2} \subset K^{H_1 \cap H_2}$. **Containment $K^{H_1 \cap H_2} \subset K^{H_1} \cdot K^{H_2}$:** We use the bijectivity of the Galois correspondence. Rather than showing the field inclusion directly (which is hard since elements of $K^{H_1 \cap H_2}$ have no explicit description in terms of elements of $K^{H_1}$ and $K^{H_2}$), we show that both fields have the same Galois group over $K$. The computation is: \begin{align*} \operatorname{Gal}(K / K^{H_1} \cdot K^{H_2}) &= \{\sigma \in G : \sigma \text{ fixes } K^{H_1} \cdot K^{H_2} \text{ pointwise}\} \\ &= \{\sigma \in G : \sigma \text{ fixes } K^{H_1} \text{ and } K^{H_2} \text{ pointwise}\} \\ &= \operatorname{Gal}(K/K^{H_1}) \cap \operatorname{Gal}(K/K^{H_2}) \\ &= H_1 \cap H_2. \end{align*} The second equality holds because the compositum $K^{H_1} \cdot K^{H_2}$ is the smallest field containing both $K^{H_1}$ and $K^{H_2}$, so fixing it pointwise is equivalent to fixing both $K^{H_1}$ and $K^{H_2}$ pointwise. Since $\operatorname{Gal}(K / K^{H_1} \cdot K^{H_2}) = H_1 \cap H_2 = \operatorname{Gal}(K / K^{H_1 \cap H_2})$, the injectivity of the Galois correspondence (the map $E \mapsto \operatorname{Gal}(K/E)$ is injective on intermediate fields) gives $K^{H_1} \cdot K^{H_2} = K^{H_1 \cap H_2}$.[/guided]

[step:Prove $K^{\langle H_1, H_2 \rangle} = K^{H_1} \cap K^{H_2}$]We again show two containments. **Containment $K^{\langle H_1, H_2 \rangle} \subset K^{H_1} \cap K^{H_2}$:** Since $H_1 \le \langle H_1, H_2 \rangle$ and $H_2 \le \langle H_1, H_2 \rangle$, the order-reversing property of $\Phi$ gives $K^{\langle H_1, H_2 \rangle} \subset K^{H_1}$ and $K^{\langle H_1, H_2 \rangle} \subset K^{H_2}$. Therefore $K^{\langle H_1, H_2 \rangle} \subset K^{H_1} \cap K^{H_2}$. **Containment $K^{H_1} \cap K^{H_2} \subset K^{\langle H_1, H_2 \rangle}$:** We compute $\operatorname{Gal}(K / K^{H_1} \cap K^{H_2})$. An automorphism $\sigma \in G$ fixes $K^{H_1} \cap K^{H_2}$ pointwise if and only if $\sigma$ fixes every element that lies in both $K^{H_1}$ and $K^{H_2}$. We claim $\operatorname{Gal}(K / K^{H_1} \cap K^{H_2}) = \langle H_1, H_2 \rangle$. Since $K^{H_1} \cap K^{H_2} \subset K^{H_1}$, we have $H_1 = \operatorname{Gal}(K/K^{H_1}) \le \operatorname{Gal}(K / K^{H_1} \cap K^{H_2})$. Similarly $H_2 \le \operatorname{Gal}(K / K^{H_1} \cap K^{H_2})$. Since $\operatorname{Gal}(K / K^{H_1} \cap K^{H_2})$ contains both $H_1$ and $H_2$, it contains $\langle H_1, H_2 \rangle$. For the reverse, let $E = K^{H_1} \cap K^{H_2}$. We have $\langle H_1, H_2 \rangle \le \operatorname{Gal}(K/E)$ (shown above). For the opposite inclusion, the first containment gives $K^{\langle H_1, H_2 \rangle} \subset E$. Since $K^{\langle H_1, H_2 \rangle} \subset E$, any automorphism fixing $E$ pointwise also fixes $K^{\langle H_1, H_2 \rangle}$ pointwise, so $\operatorname{Gal}(K/E) \le \operatorname{Gal}(K/K^{\langle H_1, H_2 \rangle}) = \langle H_1, H_2 \rangle$ (using the [quotetheorem:1274]: $\operatorname{Gal}(K/K^H) = H$). Combined with $\langle H_1, H_2 \rangle \le \operatorname{Gal}(K/E)$, we obtain $\operatorname{Gal}(K/E) = \langle H_1, H_2 \rangle$. By the bijectivity of the Galois correspondence, $E = K^{\operatorname{Gal}(K/E)} = K^{\langle H_1, H_2 \rangle}$. Therefore $K^{H_1} \cap K^{H_2} = K^{\langle H_1, H_2 \rangle}$.[/step]

[guided]This identity says the join (generated subgroup) of two subgroups maps to the meet (intersection) of the corresponding fixed fields — again the swap characteristic of an anti-isomorphism. **Containment $K^{\langle H_1, H_2 \rangle} \subset K^{H_1} \cap K^{H_2}$:** Since $H_1 \le \langle H_1, H_2 \rangle$, the order-reversing property proved in Step 1 gives $K^{\langle H_1, H_2 \rangle} \subset K^{H_1}$. Similarly, $H_2 \le \langle H_1, H_2 \rangle$ gives $K^{\langle H_1, H_2 \rangle} \subset K^{H_2}$. An element of $K^{\langle H_1, H_2 \rangle}$ lies in both $K^{H_1}$ and $K^{H_2}$, so $K^{\langle H_1, H_2 \rangle} \subset K^{H_1} \cap K^{H_2}$. **Containment $K^{H_1} \cap K^{H_2} \subset K^{\langle H_1, H_2 \rangle}$:** We use the strategy of computing the Galois group. Let $E = K^{H_1} \cap K^{H_2}$. We claim $\operatorname{Gal}(K/E) = \langle H_1, H_2 \rangle$ and prove both inclusions. First, we show $\langle H_1, H_2 \rangle \le \operatorname{Gal}(K/E)$. Since $E = K^{H_1} \cap K^{H_2} \subset K^{H_1}$, every element of $E$ is fixed by every $\sigma \in H_1 = \operatorname{Gal}(K/K^{H_1})$. Hence $H_1 \le \operatorname{Gal}(K/E)$. By the same argument with $K^{H_2}$, we get $H_2 \le \operatorname{Gal}(K/E)$. Since $\operatorname{Gal}(K/E)$ is a subgroup of $G$ containing both $H_1$ and $H_2$, it contains the subgroup they generate: $\langle H_1, H_2 \rangle \le \operatorname{Gal}(K/E)$. Second, we show $\operatorname{Gal}(K/E) \le \langle H_1, H_2 \rangle$. From the first containment, $K^{\langle H_1, H_2 \rangle} \subset E$. Since $K^{\langle H_1, H_2 \rangle} \subset E$, any $\sigma \in \operatorname{Gal}(K/E)$ fixes $E$ pointwise, hence also fixes $K^{\langle H_1, H_2 \rangle}$ pointwise. This gives \begin{align*} \operatorname{Gal}(K/E) \le \operatorname{Gal}(K / K^{\langle H_1, H_2 \rangle}) = \langle H_1, H_2 \rangle, \end{align*} where the last equality uses the [quotetheorem:1274]: $\operatorname{Gal}(K/K^H) = H$ for every $H \le G$. Combining $\langle H_1, H_2 \rangle \le \operatorname{Gal}(K/E)$ and $\operatorname{Gal}(K/E) \le \langle H_1, H_2 \rangle$, we obtain $\operatorname{Gal}(K/E) = \langle H_1, H_2 \rangle$. The Fundamental Theorem then gives $E = K^{\operatorname{Gal}(K/E)} = K^{\langle H_1, H_2 \rangle}$. Therefore $K^{H_1} \cap K^{H_2} = K^{\langle H_1, H_2 \rangle}$.[/guided]

[step:Conclude that $H \mapsto K^H$ is a lattice anti-isomorphism] We have shown: 1. The map $\Phi: H \mapsto K^H$ is a bijection from the lattice of subgroups of $G$ to the lattice of intermediate fields of $K/k$ (by the [quotetheorem:1274]). 2. $\Phi$ reverses order: $H_1 \le H_2 \iff K^{H_2} \subset K^{H_1}$. 3. $\Phi$ sends meets to joins: $K^{H_1 \cap H_2} = K^{H_1} \cdot K^{H_2}$. 4. $\Phi$ sends joins to meets: $K^{\langle H_1, H_2 \rangle} = K^{H_1} \cap K^{H_2}$. Properties (1)-(4) are precisely the definition of a lattice anti-isomorphism. The meet operation in the subgroup lattice is $\cap$, the join is $\langle \cdot, \cdot \rangle$; the meet in the field lattice is $\cap$, the join is the compositum $\cdot$. The map $\Phi$ interchanges meets and joins, so it is an anti-isomorphism of lattices. [/step]