PBW gives an ordered monomial basis for the enveloping algebra

Orient [F1] as a rewriting rule whenever $j>i$. Order words first by length and then by their number of inverted index pairs. The swapped term has one fewer inversion and the bracket term has smaller length, so every sequence of reductions terminates in a linear combination of ordered words. Hence the ordered monomials span $U(\mathfrak{g})$.

Work first in the free tensor algebra, and extend each reduction linearly and inside arbitrary word contexts. Reductions at disjoint positions join by applying both rules in either order. The only overlapping positions are the two descents in $x_k{x}_j{x}_i$ with $k>j>i$. After applying the remaining swap in each branch, their difference is $[[x_j,x_i],x_k]+[x_j,[x_k,x_i]]+[[x_k,x_j],x_i],$ where each displayed Lie bracket is obtained by reducing the corresponding two-letter commutator (and expanding its Lie-algebra value in the $x_i$ basis). All these terms have length at most two after the first reduction, so their normal forms are already determined by induction on length. The displayed expression is zero by Jacobi. Hence both branches have the same normal form.

Here is the normal-form induction needed for linear reductions. Order words by (length, inversion count); below any fixed word there are finitely many words. Define its normal form recursively as the linear combination of normal forms produced by any one reduction, with an ordered word fixed by the recursion. Induct on this order to prove independence of the chosen reduction: for two choices, step 2.1 joins their immediate descendants (inside the same surrounding context), and the induction hypothesis gives the same normal form to both joined expressions. Linearity extends the resulting map $N$ to every tensor polynomial. Each one-step reduction of a polynomial preserves $N$, because it does so term by term. In particular, every contextual defining relation $u(x_j{x}_i-x_i{x}_j-[x_j,x_i])v$ has normal form zero; so does every element of the two-sided ideal generated by these relations.

If a linear combination of distinct ordered monomials represented zero in the tensor quotient, it would lie in the defining ideal. Its normal form would be zero by step 3.1, yet $N$ fixes every ordered word and thus fixes this nonzero combination. This contradiction proves linear independence; step 1.1 supplies spanning. [step 1.1, step 3.1].

In the associated graded algebra the bracket correction in [F1] has one lower tensor degree, so the symbol of an ordered monomial depends only on the corresponding commutative monomial. Step 4.1 shows that these symbols form a basis in each degree. Therefore the natural graded map $S(\mathfrak{g})\to \mathrm{gr}U(\mathfrak{g})$ is an isomorphism.