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. 

<a href="https://www.mathnet.ru/php/archive.phtml?wshow=paper&jrnid=faa&paperid=712&option_lang=rus">text in russian</a>, <a href="https://doi.org/10.1007/BF01087537">text in English</a>