Assume HT1: T1_space R R_ray_topology.
We will prove False.
We prove the intermediate claim Hfinite_closed: ∀F : set, F ⊆ R → finite F → closed_in R R_ray_topology F.
An exact proof term for the current goal is (andER (topology_on R R_ray_topology) (∀F : set, F ⊆ R → finite F → closed_in R R_ray_topology F) HT1).
We prove the intermediate claim Hsub0: {0} ⊆ R.
Let x be given.
Assume Hx0: x ∈ {0}.
We prove the intermediate claim Hxeq: x = 0.
An exact proof term for the current goal is (SingE 0 x Hx0).
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is real_0.
We prove the intermediate claim Hfin0: finite {0}.
An exact proof term for the current goal is (Sing_finite 0).
We prove the intermediate claim Hclosed0: closed_in R R_ray_topology {0}.
An exact proof term for the current goal is (Hfinite_closed {0} Hsub0 Hfin0).
We prove the intermediate claim Hclosed0core: {0} ⊆ R ∧ ∃U ∈ R_ray_topology, {0} = R ∖ U.
An exact proof term for the current goal is (andER (topology_on R R_ray_topology) ({0} ⊆ R ∧ ∃U ∈ R_ray_topology, {0} = R ∖ U) Hclosed0).
We prove the intermediate claim HexUtyped: ∃U ∈ R_ray_topology, {0} = R ∖ U.
An exact proof term for the current goal is (andER ({0} ⊆ R) (∃U ∈ R_ray_topology, {0} = R ∖ U) Hclosed0core).
Apply HexUtyped to the current goal.
Let U be given.
Assume HUrep: U ∈ R_ray_topology ∧ {0} = R ∖ U.
We prove the intermediate claim HU: U ∈ R_ray_topology.
An exact proof term for the current goal is (andEL (U ∈ R_ray_topology) ({0} = R ∖ U) HUrep).
We prove the intermediate claim Heq: {0} = R ∖ U.
An exact proof term for the current goal is (andER (U ∈ R_ray_topology) ({0} = R ∖ U) HUrep).
We prove the intermediate claim H1in: 1 ∈ U.
We prove the intermediate claim H1not0: 1 ∉ {0}.
Assume H10: 1 ∈ {0}.
We prove the intermediate claim H10eq: 1 = 0.
An exact proof term for the current goal is (SingE 0 1 H10).
We prove the intermediate claim H00lt: 0 < 0.
rewrite the current goal using H10eq (from right to left) at position 2.
An exact proof term for the current goal is SNoLt_0_1.
An exact proof term for the current goal is ((SNoLt_irref 0) H00lt).
We will prove 1 ∈ U.
Apply (xm (1 ∈ U)) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume HnU: ¬ (1 ∈ U).
We prove the intermediate claim H1incomp: 1 ∈ R ∖ U.
An exact proof term for the current goal is (setminusI R U 1 real_1 HnU).
We prove the intermediate claim H1in0: 1 ∈ {0}.
We prove the intermediate claim Hsubst: ∀S T : set, S = T → 1 ∈ T → 1 ∈ S.
Let S and T be given.
Assume HeqST: S = T.
Assume H1inT: 1 ∈ T.
We will prove 1 ∈ S.
rewrite the current goal using HeqST (from left to right).
An exact proof term for the current goal is H1inT.
An exact proof term for the current goal is (Hsubst {0} (R ∖ U) Heq H1incomp).
Apply FalseE to the current goal.
An exact proof term for the current goal is (H1not0 H1in0).
We prove the intermediate claim H0in: 0 ∈ U.
An exact proof term for the current goal is (ray_topology_contains_0_if_contains_1 U HU H1in).
We prove the intermediate claim H0incomp: 0 ∈ R ∖ U.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is (SingI 0).
We prove the intermediate claim H0not: 0 ∉ U.
An exact proof term for the current goal is (setminusE2 R U 0 H0incomp).
An exact proof term for the current goal is (H0not H0in).
∎