Let x be given.

Assume Hx: x ∈ closure_of R R_standard_topology K_set.

We will prove x ∈ K_set ∪ {0}.

We prove the intermediate claim HxR: x ∈ R.

An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ ∀U : set, U ∈ R_standard_topology → x0 ∈ U → U ∩ K_set ≠ Empty) x Hx).

We prove the intermediate claim Hcl: ∀U : set, U ∈ R_standard_topology → x ∈ U → U ∩ K_set ≠ Empty.

An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ∀U : set, U ∈ R_standard_topology → x0 ∈ U → U ∩ K_set ≠ Empty) x Hx).

Apply (xm (x = 0)) to the current goal.

Assume Hx0: x = 0.

rewrite the current goal using Hx0 (from left to right).

An exact proof term for the current goal is (binunionI2 K_set {0} 0 (SingI 0)).

Assume Hxne0: ¬ (x = 0).

Apply (SNoLt_trichotomy_or_impred x 0 (real_SNo x HxR) SNo_0 (x ∈ K_set ∪ {0})) to the current goal.

Assume Hxlt0: x < 0.

Apply FalseE to the current goal.

Set U0 to be the term {y ∈ R|Rlt y 0}.

We prove the intermediate claim HU0: U0 ∈ R_standard_topology.

An exact proof term for the current goal is (open_left_ray_in_R_standard_topology 0 real_0).

We prove the intermediate claim HxU0: x ∈ U0.

We prove the intermediate claim HxRlt0: Rlt x 0.

An exact proof term for the current goal is (RltI x 0 HxR real_0 Hxlt0).

An exact proof term for the current goal is (SepI R (λy0 : set ⇒ Rlt y0 0) x HxR HxRlt0).

We prove the intermediate claim Hne: U0 ∩ K_set ≠ Empty.

An exact proof term for the current goal is (Hcl U0 HU0 HxU0).

We prove the intermediate claim Hempty: U0 ∩ K_set = Empty.

Apply Empty_Subq_eq to the current goal.

Let z be given.

Assume Hz: z ∈ U0 ∩ K_set.

We will prove z ∈ Empty.

Apply FalseE to the current goal.

We prove the intermediate claim HzU0: z ∈ U0.

An exact proof term for the current goal is (binintersectE1 U0 K_set z Hz).

We prove the intermediate claim HzK: z ∈ K_set.

An exact proof term for the current goal is (binintersectE2 U0 K_set z Hz).

We prove the intermediate claim Hzlt0: Rlt z 0.

An exact proof term for the current goal is (SepE2 R (λy0 : set ⇒ Rlt y0 0) z HzU0).

Apply (ReplE_impred (ω ∖ {0}) (λn : set ⇒ inv_nat n) z HzK False) to the current goal.

Let n be given.

Assume HnIn: n ∈ ω ∖ {0}.

Assume Hzeq: z = inv_nat n.

We prove the intermediate claim Hzpos: Rlt 0 z.

rewrite the current goal using Hzeq (from left to right).

An exact proof term for the current goal is (inv_nat_pos n HnIn).

We prove the intermediate claim H00: Rlt 0 0.

An exact proof term for the current goal is (Rlt_tra 0 z 0 Hzpos Hzlt0).

An exact proof term for the current goal is ((not_Rlt_refl 0 real_0) H00).

An exact proof term for the current goal is (Hne Hempty).

Assume Hxeq0: x = 0.

Apply FalseE to the current goal.

An exact proof term for the current goal is (Hxne0 Hxeq0).

Assume H0ltx: 0 < x.

Apply (xm (x ∈ K_set)) to the current goal.

Assume HxK: x ∈ K_set.

An exact proof term for the current goal is (binunionI1 K_set {0} x HxK).

Assume HxnotK: ¬ (x ∈ K_set).

Apply FalseE to the current goal.

We prove the intermediate claim HexU: ∃U : set, U ∈ R_standard_topology ∧ x ∈ U ∧ U ∩ K_set = Empty.

An exact proof term for the current goal is (standard_open_neighborhood_disjoint_from_K_set_pos x HxR H0ltx HxnotK).

Apply HexU to the current goal.

Let U be given.

Assume HUpair.

We prove the intermediate claim HUleft: U ∈ R_standard_topology ∧ x ∈ U.

An exact proof term for the current goal is (andEL (U ∈ R_standard_topology ∧ x ∈ U) (U ∩ K_set = Empty) HUpair).

We prove the intermediate claim HU: U ∈ R_standard_topology.

An exact proof term for the current goal is (andEL (U ∈ R_standard_topology) (x ∈ U) HUleft).

We prove the intermediate claim HxU: x ∈ U.

An exact proof term for the current goal is (andER (U ∈ R_standard_topology) (x ∈ U) HUleft).

We prove the intermediate claim Hne: U ∩ K_set ≠ Empty.

An exact proof term for the current goal is (Hcl U HU HxU).

We prove the intermediate claim HUempty: U ∩ K_set = Empty.

An exact proof term for the current goal is (andER (U ∈ R_standard_topology ∧ x ∈ U) (U ∩ K_set = Empty) HUpair).

An exact proof term for the current goal is (Hne HUempty).

Let x be given.

Assume Hx: x ∈ K_set ∪ {0}.

We will prove x ∈ closure_of R R_standard_topology K_set.

Apply (binunionE' K_set {0} x (x ∈ closure_of R R_standard_topology K_set)) to the current goal.

Assume HxK: x ∈ K_set.

We prove the intermediate claim HKsub: K_set ⊆ R.

An exact proof term for the current goal is K_set_Subq_R.

We prove the intermediate claim Hsub: K_set ⊆ closure_of R R_standard_topology K_set.

An exact proof term for the current goal is (subset_of_closure R R_standard_topology K_set R_standard_topology_is_topology_local HKsub).

An exact proof term for the current goal is (Hsub x HxK).

Assume Hx0: x ∈ {0}.

We prove the intermediate claim Hxeq0: x = 0.

An exact proof term for the current goal is (SingE 0 x Hx0).

rewrite the current goal using Hxeq0 (from left to right).

We will prove 0 ∈ closure_of R R_standard_topology K_set.

We prove the intermediate claim Hcl: ∀U : set, U ∈ R_standard_topology → 0 ∈ U → U ∩ K_set ≠ Empty.

Let U be given.

Assume HU: U ∈ R_standard_topology.

Assume H0U: 0 ∈ U.

We will prove U ∩ K_set ≠ Empty.

We prove the intermediate claim HUprop: ∀x0 ∈ U, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U.

An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U0) U HU).

We prove the intermediate claim Hexb0: ∃b0 ∈ R_standard_basis, 0 ∈ b0 ∧ b0 ⊆ U.

An exact proof term for the current goal is (HUprop 0 H0U).

Apply Hexb0 to the current goal.

Let b0 be given.

Assume Hb0pair.

We prove the intermediate claim Hb0Std: b0 ∈ R_standard_basis.

An exact proof term for the current goal is (andEL (b0 ∈ R_standard_basis) (0 ∈ b0 ∧ b0 ⊆ U) Hb0pair).

We prove the intermediate claim Hb0rest: 0 ∈ b0 ∧ b0 ⊆ U.

An exact proof term for the current goal is (andER (b0 ∈ R_standard_basis) (0 ∈ b0 ∧ b0 ⊆ U) Hb0pair).

We prove the intermediate claim H0b0: 0 ∈ b0.

An exact proof term for the current goal is (andEL (0 ∈ b0) (b0 ⊆ U) Hb0rest).

We prove the intermediate claim Hb0subU: b0 ⊆ U.

An exact proof term for the current goal is (andER (0 ∈ b0) (b0 ⊆ U) Hb0rest).

We prove the intermediate claim Hexa: ∃a ∈ R, b0 ∈ {open_interval a b|b ∈ R}.

An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 b|b ∈ R}) b0 Hb0Std).

Apply Hexa to the current goal.

Let a be given.

Assume Hapair.

We prove the intermediate claim HaR: a ∈ R.

An exact proof term for the current goal is (andEL (a ∈ R) (b0 ∈ {open_interval a b|b ∈ R}) Hapair).

We prove the intermediate claim Hb0fam: b0 ∈ {open_interval a b|b ∈ R}.

An exact proof term for the current goal is (andER (a ∈ R) (b0 ∈ {open_interval a b|b ∈ R}) Hapair).

We prove the intermediate claim Hexb: ∃b ∈ R, b0 = open_interval a b.

An exact proof term for the current goal is (ReplE R (λb0' : set ⇒ open_interval a b0') b0 Hb0fam).

Apply Hexb to the current goal.

Let b be given.

Assume Hbpair.

We prove the intermediate claim HbR: b ∈ R.

An exact proof term for the current goal is (andEL (b ∈ R) (b0 = open_interval a b) Hbpair).

We prove the intermediate claim Hb0eq: b0 = open_interval a b.

An exact proof term for the current goal is (andER (b ∈ R) (b0 = open_interval a b) Hbpair).

We prove the intermediate claim H0in: 0 ∈ open_interval a b.

rewrite the current goal using Hb0eq (from right to left).

An exact proof term for the current goal is H0b0.

We prove the intermediate claim H0prop: Rlt a 0 ∧ Rlt 0 b.

An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 b) 0 H0in).

We prove the intermediate claim Ha0: Rlt a 0.

An exact proof term for the current goal is (andEL (Rlt a 0) (Rlt 0 b) H0prop).

We prove the intermediate claim H0b: Rlt 0 b.

An exact proof term for the current goal is (andER (Rlt a 0) (Rlt 0 b) H0prop).

We prove the intermediate claim Hexy: ∃y : set, y ∈ halfopen_interval_left 0 b ∧ y ∈ K_set.

An exact proof term for the current goal is (K_set_meets_lower_limit_neighborhood_0 0 b real_0 HbR (not_Rlt_refl 0 real_0) H0b).

Apply Hexy to the current goal.

Let y be given.

Assume Hypair.

We prove the intermediate claim Hyhalf: y ∈ halfopen_interval_left 0 b.

An exact proof term for the current goal is (andEL (y ∈ halfopen_interval_left 0 b) (y ∈ K_set) Hypair).

We prove the intermediate claim HyK: y ∈ K_set.

An exact proof term for the current goal is (andER (y ∈ halfopen_interval_left 0 b) (y ∈ K_set) Hypair).

We prove the intermediate claim HyR: y ∈ R.

An exact proof term for the current goal is (K_set_Subq_R y HyK).

We prove the intermediate claim Hyltb: Rlt y b.

An exact proof term for the current goal is (andER (¬ (Rlt y 0)) (Rlt y b) (SepE2 R (λz : set ⇒ ¬ (Rlt z 0) ∧ Rlt z b) y Hyhalf)).

We prove the intermediate claim Hypos: Rlt 0 y.

Apply (ReplE_impred (ω ∖ {0}) (λn : set ⇒ inv_nat n) y HyK (Rlt 0 y)) to the current goal.

Let n be given.

Assume HnIn: n ∈ ω ∖ {0}.

Assume Hyeq: y = inv_nat n.

rewrite the current goal using Hyeq (from left to right).

An exact proof term for the current goal is (inv_nat_pos n HnIn).

We prove the intermediate claim Hay: Rlt a y.

An exact proof term for the current goal is (Rlt_tra a 0 y Ha0 Hypos).

We prove the intermediate claim HyinInt: y ∈ open_interval a b.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt a z ∧ Rlt z b) y HyR (andI (Rlt a y) (Rlt y b) Hay Hyltb)).

We prove the intermediate claim Hyb0: y ∈ b0.

rewrite the current goal using Hb0eq (from left to right).

An exact proof term for the current goal is HyinInt.

We prove the intermediate claim HyU: y ∈ U.

An exact proof term for the current goal is (Hb0subU y Hyb0).

We prove the intermediate claim HyInt: y ∈ U ∩ K_set.

An exact proof term for the current goal is (binintersectI U K_set y HyU HyK).

An exact proof term for the current goal is (elem_implies_nonempty (U ∩ K_set) y HyInt).

An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ∀U : set, U ∈ R_standard_topology → x0 ∈ U → U ∩ K_set ≠ Empty) 0 real_0 Hcl).

An exact proof term for the current goal is Hx.