Corollary
Tag 0B7Z, permanent. Cite it as [Bourbaki, Tag 0B7Z].
General Topology, chapter I, § 9. Compact spaces and locally compact spaces
Every compact space is regular.
For it follows from axiom (Hi) (§ 8, no. 1, Proposition 1) that the filter base formed by all the closed neighbourhoods of an arbitrary point of the space satisfies the condition of Proposition 1.
The following proposition amplifies the Corollary to Proposition 1:
Bourbaki puts the proof directly after the statement, so what is above is the statement and its proof together.