We prove the intermediate claim Htop: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology_local.
Apply (iffER (T1_space R R_standard_topology) (∀z : set, z ∈ R → closed_in R R_standard_topology {z}) (lemma_T1_singletons_closed R R_standard_topology Htop)) to the current goal.
We will prove ∀z : set, z ∈ R → closed_in R R_standard_topology {z}.
Let z be given.
Assume HzR: z ∈ R.
We will prove closed_in R R_standard_topology {z}.
We prove the intermediate claim HzSub: {z} ⊆ R.
Let y be given.
Assume Hy: y ∈ {z}.
We prove the intermediate claim Heq: y = z.
An exact proof term for the current goal is (SingE z y Hy).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HzR.
We prove the intermediate claim HUopen: R ∖ {z} ∈ R_standard_topology.
rewrite the current goal using (Sing_eq_UPair z) (from left to right).
An exact proof term for the current goal is (R_minus_singleton_in_R_standard_topology z HzR).
We prove the intermediate claim Hclosed: closed_in R R_standard_topology (R ∖ (R ∖ {z})).
An exact proof term for the current goal is (closed_of_open_complement R R_standard_topology (R ∖ {z}) Htop HUopen).
We prove the intermediate claim Heq: R ∖ (R ∖ {z}) = {z}.
An exact proof term for the current goal is (setminus_setminus_eq R {z} HzSub).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hclosed.
∎