Another proof is given here; Positelsky, L, Functional Analysis and Its Applications, 1993, 27:3, 197–204 :
I quote:
''The classical PBW theorem attains its natural place in this context as a particular case of the fact that every Kozsul CDG-algebra corresponds to a QLS-algebra; here a QLS=quadratic linear scalar algebra is roughly ``an algebra defined by (generators and) non-homogenious relations of degree 2.
