Topological properties of ℝ

We show that the only closed subfield of ℝ is ℝ.

theorem Real.subfield_eq_of_closed {K : Subfield ℝ} (hc : IsClosed ↑K) : K = ⊤