Let x be given.

Assume Hx: x ∈ closure_of R R_upper_limit_topology K_set.

We will prove x ∈ K_set.

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_upper_limit_topology → x0 ∈ U → U ∩ K_set ≠ Empty) x Hx).

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

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

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

Assume HxK: x ∈ K_set.

An exact proof term for the current goal is HxK.

Assume HxnotK: ¬ (x ∈ K_set).

Apply FalseE to the current goal.

We prove the intermediate claim HxS: SNo x.

An exact proof term for the current goal is (real_SNo x HxR).

Apply (SNoLt_trichotomy_or_impred x 0 HxS SNo_0 False) to the current goal.

Assume Hxlt0: x < 0.

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

We prove the intermediate claim HU0std: 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 Hcont: finer_than R_upper_limit_topology R_standard_topology.

We prove the intermediate claim Hall: (((finer_than R_upper_limit_topology R_standard_topology ∧ finer_than R_K_topology R_standard_topology) ∧ finer_than R_standard_topology R_finite_complement_topology) ∧ finer_than R_standard_topology R_ray_topology).

An exact proof term for the current goal is ex13_7_R_topology_containments.

We prove the intermediate claim Hleft: ((finer_than R_upper_limit_topology R_standard_topology ∧ finer_than R_K_topology R_standard_topology) ∧ finer_than R_standard_topology R_finite_complement_topology).

An exact proof term for the current goal is (andEL ((finer_than R_upper_limit_topology R_standard_topology ∧ finer_than R_K_topology R_standard_topology) ∧ finer_than R_standard_topology R_finite_complement_topology) (finer_than R_standard_topology R_ray_topology) Hall).

We prove the intermediate claim Hpair: (finer_than R_upper_limit_topology R_standard_topology ∧ finer_than R_K_topology R_standard_topology).

An exact proof term for the current goal is (andEL (finer_than R_upper_limit_topology R_standard_topology ∧ finer_than R_K_topology R_standard_topology) (finer_than R_standard_topology R_finite_complement_topology) Hleft).

An exact proof term for the current goal is (andEL (finer_than R_upper_limit_topology R_standard_topology) (finer_than R_K_topology R_standard_topology) Hpair).

We prove the intermediate claim HU0: U0 ∈ R_upper_limit_topology.

An exact proof term for the current goal is (Hcont U0 HU0std).

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 Hx0: x = 0.

Set U1 to be the term halfopen_interval_right (minus_SNo 1) 0.

We prove the intermediate claim Hm1R: minus_SNo 1 ∈ R.

An exact proof term for the current goal is (real_minus_SNo 1 real_1).

We prove the intermediate claim Hm10: Rlt (minus_SNo 1) 0.

An exact proof term for the current goal is (RltI (minus_SNo 1) 0 Hm1R real_0 minus_1_lt_0).

We prove the intermediate claim HU1basis: U1 ∈ R_upper_limit_basis.

We prove the intermediate claim HU1fam: U1 ∈ {halfopen_interval_right (minus_SNo 1) b|b ∈ R}.

An exact proof term for the current goal is (ReplI R (λb0 : set ⇒ halfopen_interval_right (minus_SNo 1) b0) 0 real_0).

An exact proof term for the current goal is (famunionI R (λa0 : set ⇒ {halfopen_interval_right a0 b|b ∈ R}) (minus_SNo 1) U1 Hm1R HU1fam).

We prove the intermediate claim HU1: U1 ∈ R_upper_limit_topology.

An exact proof term for the current goal is (basis_in_generated R R_upper_limit_basis U1 R_upper_limit_basis_is_basis_local HU1basis).

We prove the intermediate claim H0U1: 0 ∈ U1.

An exact proof term for the current goal is (halfopen_interval_right_rightmem (minus_SNo 1) 0 Hm10).

We prove the intermediate claim HxU1: x ∈ U1.

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

An exact proof term for the current goal is H0U1.

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

An exact proof term for the current goal is (Hcl U1 HU1 HxU1).

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

Apply Empty_Subq_eq to the current goal.

Let z be given.

Assume Hz: z ∈ U1 ∩ K_set.

We will prove z ∈ Empty.

Apply FalseE to the current goal.

We prove the intermediate claim HzU1: z ∈ U1.

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

We prove the intermediate claim HzK: z ∈ K_set.

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

We prove the intermediate claim Hzprop: Rlt (minus_SNo 1) z ∧ ¬ (Rlt 0 z).

An exact proof term for the current goal is (SepE2 R (λy0 : set ⇒ Rlt (minus_SNo 1) y0 ∧ ¬ (Rlt 0 y0)) z HzU1).

We prove the intermediate claim Hnot0z: ¬ (Rlt 0 z).

An exact proof term for the current goal is (andER (Rlt (minus_SNo 1) z) (¬ (Rlt 0 z)) Hzprop).

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).

An exact proof term for the current goal is (Hnot0z Hzpos).

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

Assume H0ltx: 0 < x.

We prove the intermediate claim Hcont: finer_than R_upper_limit_topology R_standard_topology.

An exact proof term for the current goal is ex13_7_R_topology_containments.

We prove the intermediate claim Hpair: (finer_than R_upper_limit_topology R_standard_topology ∧ finer_than R_K_topology R_standard_topology).

An exact proof term for the current goal is (andEL (finer_than R_upper_limit_topology R_standard_topology) (finer_than R_K_topology R_standard_topology) Hpair).

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 HUstd: 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 HU: U ∈ R_upper_limit_topology.

An exact proof term for the current goal is (Hcont U HUstd).

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).