Corollary 1
Tag 06KC, permanent. Cite it as [Bourbaki, Tag 06KC].
Algebra, chapter V, § 7. Separable algebraic extensions
— If an element x of E is a simple root of a polynomial g of K[X], it is separable over K. For the minimal polynomial f of x over K divides g in K[X] (V, p. 16, Th. 1), so x is a simple root of f.
Bourbaki puts the proof directly after the statement, so what is above is the statement and its proof together.