# Proof that Effros Borel space is standard

I have difficulty understanding the proof of Theorem 12.6 in Kechris's Classical Descriptive Set Theory that if $$X$$ is Polish then the Effros Borel space of $$F(X)$$ is standard. $$F(X)$$ consists of all closed sets in $$X$$, and I am not giving the definition of Effros Borel space since it is probably not so related to my confusion. The proof proceeds as follows:

1. Let $$\overline{X}$$ be a compactification of $$X$$.
2. Identify $$F(X)$$ with a subset $$G$$ of $$K(\overline{X})$$, the collection of compact sets in $$\overline{X}$$.
3. Prove that $$G$$ is $$G_\delta$$ in $$K(\overline{X})$$, hence Polish.
4. Carry the topology on $$G$$ back to $$F(X)$$. Prove that Effros Borel space coincides with the topology.

I guess in 3 the author implicitly assumes that $$K(\overline{X})$$ is Polish, which seems to depend on the metrizability of $$\overline{X}$$. But why is it metrizable? Certainly not any compactification works, for example the Stone–Čech compactification of $$\mathbb{N}$$ is not even first countable; I think the one-point compactification of $$\mathbb{R}^{\mathbb{N}}$$ is not first countable either. Can every Polish space be embedded into some compact metric space?

This is what Theorem $$4.14$$ does:
This gives the desired embedding result. Note that Kechris uses a nonstandard (in my experience) notion of "compactification," in Definition $$4.15$$: a compactification of a separable metrizable space $$X$$ is a compact metrizable space $$Y$$ such that $$X$$ is homeomorphic to a dense subset of $$Y$$. So the "pick a compactification" language in the proof in question is unproblematic ... if we grant Kechris' use of the term.