Let x be given.

Assume Hx: x ∈ closure_of R R_K_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_K_topology → x0 ∈ U → U ∩ K_set ≠ Empty) x Hx).

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

An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ∀U : set, U ∈ R_K_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 HexI: ∃I ∈ R_standard_basis, x ∈ I.

An exact proof term for the current goal is (basis_on_cover R R_standard_basis R_standard_basis_is_basis_local x HxR).

Apply HexI to the current goal.

Let I be given.

Assume HIpair.

We prove the intermediate claim HIstd: I ∈ R_standard_basis.

An exact proof term for the current goal is (andEL (I ∈ R_standard_basis) (x ∈ I) HIpair).

We prove the intermediate claim HxI: x ∈ I.

An exact proof term for the current goal is (andER (I ∈ R_standard_basis) (x ∈ I) HIpair).

We prove the intermediate claim Hexa: ∃a ∈ R, I ∈ {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}) I HIstd).

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) (I ∈ {open_interval a b|b ∈ R}) Hapair).

We prove the intermediate claim HIfam: I ∈ {open_interval a b|b ∈ R}.

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

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

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

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) (I = open_interval a b) Hbpair).

We prove the intermediate claim HIeq: I = open_interval a b.

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

Set U to be the term open_interval a b ∖ K_set.

We prove the intermediate claim HUopen: U ∈ R_K_topology.

We prove the intermediate claim HUk: U ∈ R_K_basis.

We prove the intermediate claim HUr: U ∈ {open_interval a b0 ∖ K_set|b0 ∈ R}.

An exact proof term for the current goal is (ReplI R (λb0 : set ⇒ open_interval a b0 ∖ K_set) b HbR).

An exact proof term for the current goal is (famunionI R (λa0 : set ⇒ {open_interval a0 b0 ∖ K_set|b0 ∈ R}) a U HaR HUr).

We prove the intermediate claim HUinB: U ∈ (R_standard_basis ∪ R_K_basis).

An exact proof term for the current goal is (binunionI2 R_standard_basis R_K_basis U HUk).

An exact proof term for the current goal is (basis_in_generated R (R_standard_basis ∪ R_K_basis) U R_standard_plus_K_basis_is_basis_local HUinB).

We prove the intermediate claim HxU: x ∈ U.

We prove the intermediate claim HxOpen: x ∈ open_interval a b.

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

An exact proof term for the current goal is HxI.

An exact proof term for the current goal is (setminusI (open_interval a b) K_set x HxOpen HxnotK).

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

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

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

Apply Empty_Subq_eq to the current goal.

Let y be given.

Assume Hy: y ∈ U ∩ K_set.

We will prove y ∈ Empty.

Apply FalseE to the current goal.

We prove the intermediate claim HyU: y ∈ U.

An exact proof term for the current goal is (binintersectE1 U K_set y Hy).

We prove the intermediate claim HyK: y ∈ K_set.

An exact proof term for the current goal is (binintersectE2 U K_set y Hy).

We prove the intermediate claim HyNotK: y ∉ K_set.

An exact proof term for the current goal is (setminusE2 (open_interval a b) K_set y HyU).

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

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