Coadjoint orbits are symplectic manifolds

By [F1] the KKS prescription gives, at every $\beta \in \mathcal{O}$, an alternating bilinear form on $T_{\beta }\mathcal{O}$, because the bracket is bilinear and alternating.

Smoothness: fix ${\beta }_0\in \mathcal{O}$ and, using [F2], choose finitely many ${\xi }_1,\dots ,{\xi }_k\in \mathfrak{g}$ whose fields ${\xi }_{i\mathcal{O}}({\beta }_0)$ form a basis of $T_{{\beta }_0}\mathcal{O}$. By continuity the same fields are linearly independent on a neighbourhood $U$ of ${\beta }_0$, and they are smooth by [F2], so they form a smooth frame of $T\mathcal{O}{\mathrm{\mid }}_U$. On $U$ the frame values $\omega ({\xi }_{i\mathcal{O}},{\xi }_{j\mathcal{O}})={\mathrm{\Phi }}^{[{\xi }_i,{\xi }_j]}$ are smooth functions, and expanding two smooth fields in the frame with smooth coefficients shows that $\omega$ is smooth on $U$; such neighbourhoods cover $\mathcal{O}$.

Nondegeneracy: let $\beta \in \mathcal{O}$ and suppose ${\omega }_{\beta }({\xi }_{\mathcal{O}}(\beta ),{\eta }_{\mathcal{O}}(\beta ))=0$ for all $\eta \in \mathfrak{g}$. Then $\beta ([\xi ,\eta ])=0$ for all $\eta$, so ${\xi }_{{\mathfrak{g}}^{\ast }}(\beta )=0$ by [F3], so $\xi \in {\mathfrak{g}}_{\beta }$ and ${\xi }_{\mathcal{O}}(\beta )=0$ by [F2]. Hence the radical of ${\omega }_{\beta }$ is zero.

$G$-invariance: for $h\in G$ and $\beta \in \mathcal{O}$, step 1.1 and [F4] give ${\omega }_{h\cdot \beta }(d(a_h{)}_{\beta }{\xi }_{\mathcal{O}}(\beta ),d(a_h{)}_{\beta }{\eta }_{\mathcal{O}}(\beta ))={\omega }_{h\cdot \beta }(({\mathrm{Ad}}_h\xi {)}_{\mathcal{O}}(h\cdot \beta ),({\mathrm{Ad}}_h\eta {)}_{\mathcal{O}}(h\cdot \beta ))=(h\cdot \beta )([{\mathrm{Ad}}_h\xi ,{\mathrm{Ad}}_h\eta ])=\beta ([\xi ,\eta ])={\omega }_{\beta }({\xi }_{\mathcal{O}}(\beta ),{\eta }_{\mathcal{O}}(\beta ))\mathrm{.}$

The inclusion satisfies the moment equation: for $\zeta \in \mathfrak{g}$ and $\beta \in \mathcal{O}$, [F6] and [F3] give $d{\mathrm{\Phi }}_{\beta }^{\zeta }({\eta }_{\mathcal{O}}(\beta ))={\eta }_{\mathcal{O}}(\beta )(\zeta )=\beta ([\eta ,\zeta ])=-\beta ([\zeta ,\eta ])=-{\omega }_{\beta }({\zeta }_{\mathcal{O}}(\beta ),{\eta }_{\mathcal{O}}(\beta ))\mathrm{.}$ Since the vectors ${\eta }_{\mathcal{O}}(\beta )$ span $T_{\beta }\mathcal{O}$ by [F2], this is exactly ${\iota }_{{\zeta }_{\mathcal{O}}}\omega =-d{\mathrm{\Phi }}^{\zeta }$.

Closedness: the flow of ${\xi }_{\mathcal{O}}$ is the action of the one-parameter group ${\exp }_G(-t\xi )$, which preserves $\omega$ by step 2.3, so ${\mathcal{L}}_{{\xi }_{\mathcal{O}}}\omega =0$ by [F5]. By step 2.4 the one-form ${\iota }_{{\xi }_{\mathcal{O}}}\omega =-d{\mathrm{\Phi }}^{\xi }$ is exact, hence closed. Cartan's formula [F5] gives ${\iota }_{{\xi }_{\mathcal{O}}}d\omega ={\mathcal{L}}_{{\xi }_{\mathcal{O}}}\omega -d{\iota }_{{\xi }_{\mathcal{O}}}\omega =0$; since the fields ${\xi }_{\mathcal{O}}$ span each tangent space by [F2], $d\omega =0$.

Uniqueness: let ${\omega }^{\mathrm{\prime }}$ be any two-form on $\mathcal{O}$ for which the inclusion satisfies the same component moment equations. Then for all $\beta ,\xi ,\eta$, ${\omega }_{\beta }^{\mathrm{\prime }}({\xi }_{\mathcal{O}}(\beta ),{\eta }_{\mathcal{O}}(\beta ))=-{\omega }_{\beta }^{\mathrm{\prime }}({\eta }_{\mathcal{O}}(\beta ),{\xi }_{\mathcal{O}}(\beta ))=d{\mathrm{\Phi }}_{\beta }^{\eta }({\xi }_{\mathcal{O}}(\beta ))={\xi }_{\mathcal{O}}(\beta )(\eta )=\beta ([\xi ,\eta ])={\omega }_{\beta }({\xi }_{\mathcal{O}}(\beta ),{\eta }_{\mathcal{O}}(\beta )),$ and the fundamental fields span each tangent space by [F2], so ${\omega }^{\mathrm{\prime }}=\omega$.