Every integrable weight is weyl conjugate toward the dominant chamber

First every weight $\mu$ of an integrable module is integral. Fix $i$ and choose the largest $r\ge 0$ with $u=e_i^{r}v\mathrm{\ne }0$ using F6. Then $e_{i}u=0$ and $h_{i}u=au$ where $a=\mu (h_i)+2r$ by F7. The recurrence $e_i{f}_i^{m+1}u=f_i{e}_i{f}_i^{m}u+h_i{f}_i^{m}u$, with $h_i{f}_i^{m}u=(a-2m)f_i^{m}u$, gives $e_i{f}_i^{m}u=m(a-m+1)f_i^{m-1}u$ by induction from $e_{i}u=0$. If $N$ is the least positive exponent killing $u$ under $f_i$, F6 supplies it and $f_i^{N-1}u\mathrm{\ne }0$. Therefore $0=N(a-N+1)f_i^{N-1}u$ implies $a=N-1$, so $\mu (h_i)=N-1-2r\in \mathbb{Z}$. Apply this to each $i$ and use F2.

If the orbit already meets $P^{+}$, apply F5 using 1.1. It proves termination under any negative-label choices, uniqueness of $\eta$, and the precise stabilizer formula. If $w\mu =\eta$, every product $zw$ with $z\in {\mathrm{Stab}}_W(\eta )$ also transports $\mu$ to $\eta$, explaining the possible nonuniqueness without weakening dominant uniqueness.

Now assume $V\in \mathcal{O}$. Whenever the current weight $\nu$ has a negative simple label, F4 changes it to $\nu +k{\alpha }_i$ for the positive integer $k=-\nu (h_i)$, using 1.1. By F1 it remains a support weight. Thus repeated reflections at, for example, the least negative index form a strictly increasing chain of support weights above the original $\mu$. The independence of simple roots makes each increase strict in the positive-root order. F3 supplies only finitely many such weights, so the process must stop, necessarily with every label nonnegative. By F2 the endpoint is dominant integral. Hence the orbit meets $P^{+}$.

If $V$ is integrable highest weight, F8 and the quotient clause of F3 put it in $\mathcal{O}$, so 2.2 applies. The zero module has no weights to consider. A dominant starting weight requires zero reflections, and label zero is never selected by the procedure. Rank one is covered by the same finite string calculation in 1.1. All nilpotence bounds are least or largest integers for fixed vectors; the procedure uses least indices, and the argument uses only F1's actual isomorphisms, so no AC is consumed. An arbitrary integral orbit not meeting $P^{+}$ is outside the conditional assertion.