Chỉ cần chứng minh rằng hợp của hai tập không trù mật $A, B$ là không trù mật, và không mất tính tổng quát, ta có thể giả sử rằng $A$ và $B$ là đóng. Khi đó mệnh đề tương đương với việc nói rằng giao của hai tập mở trù mật $\overline{C}A, \overline{C}B$ là trù mật. Nếu $U$ là một tập mở không rỗng, thì $U \cap \overline{C}A$ là mở và không rỗng, do đó

là mở và không rỗng.

Cho $Y$ là một không gian con của một không gian tôpô $X$. Một không gian con $A$ của $Y$ được gọi là không trù mật tương đối đối với $Y$ nếu $A$ là không trù mật khi được xét như một tập con của không gian tôpô $Y$.

Giả sử rằng $A$ không trù mật tương đối đối với $Y$. Nếu bao đóng $\overline{A}$ của $A$ trong $X$ chứa một tập mở không rỗng $U$, thì $U \cap A$ không rỗng (theo định nghĩa của bao đóng); do đó $U \cap Y$ là một tập mở không rỗng tương đối đối với $Y$, và được chứa trong bao đóng $\overline{A} \cap Y$ của $A$ đối với $Y$, trái với giả thiết.

Bây giờ giả sử rằng $Y$ là mở trong $X$ và $A \subset Y$ là không trù mật nơi nào tương đối với $X$. Nếu $U$ là mở trong $Y$ và không rỗng, thì $U$ là mở trong $X$ và do đó chứa một tập hợp $V$ không rỗng, mở trong $X$ (và a fortiori trong $Y$) và không giao với $A$; suy ra $A$ là không trù mật nơi nào tương đối với $Y$.

Phần thứ hai của Mệnh đề 2 rõ ràng không đúng nếu $Y$ không mở trong $X$; xét, chẳng hạn, trường hợp $Y \neq \emptyset$ là không trù mật nơi nào trong $X$, và $A = Y$.

Điều này suy ra từ (EB"), vì mọi tập hợp mở (t.ư. thưa) trong $Y$ đều mở (t.ư. thưa) trong $X$.

Theo Mệnh đề 3, mọi điểm của một không gian Baire đều có một hệ cơ sở các lân cận, mỗi lân cận trong đó là một không gian Baire. Ngược lại:

Cho $A$ là một tập mở không rỗng trong $X$, cho $x \in A$ và cho $V$ là một lân cận mở của $x$ là một không gian Baire. Nếu $A$ là tập loại thứ nhất trong $X$, thì $V \cap A$ sẽ là tập loại thứ nhất trong $V$ và mở trong $V$, điều này trái với giả thiết.

Cho $A$ là một tập loại thứ nhất trong $X$; khi đó phần bù $Y = \complement_A$ của nó trong $X$ là trù mật trong $X$. Cho $B$ là một tập loại thứ nhất tương đối đối với $Y$; $B$ cũng là tập loại thứ nhất tương đối đối với $X$, do đó $A \cup B$ là tập loại thứ nhất tương đối đối với $X$. Vì vậy phần bù của $A \cup B$ trong $X$, cũng là phần bù của $B$ trong $Y$, là trù mật trong $X$ và a fortiori trù mật trong $Y$. Do đó $Y$ là một không gian Baire.

Ta sẽ chứng minh rằng tiên đề (EB) được thỏa mãn trong mỗi trường hợp. Cho $(A_n)$ là một dãy các tập mở trù mật trong $X$, và cho $G$ là một tập mở không rỗng bất kỳ. Khi đó ta có thể định nghĩa quy nạp một dãy $(G_n)$ các tập mở không rỗng sao cho $G_1 = G$ và $\overline{G}_{n+1} \subset G_n \cap A_n$: vì theo giả thiết $G_n$ không rỗng, nên $G_n \cap A_n$ là một tập mở không rỗng; và vì $X$ là chính quy trong cả hai trường hợp được xét, nên tồn tại một tập mở không rỗng $G_{n+1}$ sao cho $\overline{G}_{n+1} \subset G_n \cap A_n$. Do đó tập $G \cap \bigcap_{n=1}^\infty A_n$ chứa giao của các tập $G_n$, bằng giao của các tập $\overline{G}_n$; vì vậy chỉ cần chứng minh rằng $\bigcap_{n=1}^\infty \overline{G}_n \neq \varnothing$. Bây giờ nếu $X$ là địa phương compact, ta có thể giả sử rằng $\overline{G}_2$ là compact; trong không gian compact $\overline{G}_2$, các $\overline{G}_n (n \geq 2)$ tạo thành một dãy giảm các tập đóng không rỗng, và giao của chúng do đó không rỗng theo tiên đề (C'') (xem Chương I, § 9, no. 1, Định nghĩa 1]. Nếu $X$ là một không gian mêtric đầy đủ (đối với một mêtric tương thích với tôpô của nó), ta có thể giả sử rằng $\overline{G}_n$ đã được chọn sao cho đường kính của nó (đối với mêtric này) dần về 0 khi $n$ dần tới $+\infty$; do đó các $\overline{G}_n$ tạo thành một cơ sở lọc Cauchy hội tụ đến một điểm $x$, và $x$ nhất thiết thuộc giao của các tập $\overline{G}_n$.

Q.E.D.

Định lý này cũng có thể được phát biểu dưới dạng: tập hợp các điểm mà trong một lân cận của chúng họ $(f_\alpha)$ bị chặn trên đều là một tập hợp mở trù mật.

Cho $f = \sup_\alpha f_\alpha$ là bao trên của họ $(f_\alpha)$. Hàm $f$ là nửa liên tục dưới (Chương IV, § 6, no. 2, Định lý 4) và hữu hạn tại mọi điểm của $X$. Vì vậy chỉ cần thực hiện chứng minh trong trường hợp họ $(f_\alpha)$ gồm một hàm duy nhất $f$. Gọi $A_n$ là tập hợp các điểm $x \in X$ sao cho $f(x) \leq n$; $A_n$ là đóng (Chương IV, § 6, no. 2, Mệnh đề 1), và các giả thiết suy ra rằng $X$ là hợp của các tập hợp $A_n$; do đó ít nhất một trong các $A_n$ có một điểm trong, và vì vậy tồn tại một tập hợp mở không rỗng trên đó $f$ bị chặn trên (bởi một số nguyên $n$). Nếu áp dụng kết quả này cho mọi tập hợp con mở không rỗng của $X$ (không gian con này cũng là một không gian Baire theo Mệnh đề 3 của no. 3), ta có định lý.

Trong các áp dụng của định lý này, nói chung các $f_\alpha$ là liên tục trên $X$.