Corollary
Tag 06KG, permanent. Cite it as [Bourbaki, Tag 06KG].
Algebra, chapter V, § 7. Separable algebraic extensions
— For an algebraic extension E to be separable over K it is necessary and sufficient that every element of E should be a simple root of its minimal polynomial over K. It is enough to apply Prop. 5 and 6.
Bourbaki puts the proof directly after the statement, so what is above is the statement and its proof together.