Let U be given.

Assume HUsub: U ⊆ Tx.

Assume HUcount: countable_set U.

Assume HUdense: ∀u : set, u ∈ U → u ∈ Tx ∧ dense_in u X Tx.

We will prove dense_in (intersection_over_family X U) X Tx.

Set Fam to be the term {X ∖ u|u ∈ U}.

We prove the intermediate claim HFamcount: countable_set Fam.

An exact proof term for the current goal is (countable_image U HUcount (λu0 : set ⇒ X ∖ u0)).

We prove the intermediate claim HFamprop: ∀A : set, A ∈ Fam → closed_in X Tx A ∧ interior_of X Tx A = Empty.

Let A be given.

Assume HA: A ∈ Fam.

We prove the intermediate claim Hexu: ∃u : set, u ∈ U ∧ A = X ∖ u.

An exact proof term for the current goal is (ReplE U (λu0 : set ⇒ X ∖ u0) A HA).

Apply Hexu to the current goal.

Let u be given.

Assume Hu: u ∈ U ∧ A = X ∖ u.

We prove the intermediate claim HuU: u ∈ U.

An exact proof term for the current goal is (andEL (u ∈ U) (A = X ∖ u) Hu).

We prove the intermediate claim HAeq: A = X ∖ u.

An exact proof term for the current goal is (andER (u ∈ U) (A = X ∖ u) Hu).

We prove the intermediate claim Hup: u ∈ Tx ∧ dense_in u X Tx.

An exact proof term for the current goal is (HUdense u HuU).

We prove the intermediate claim HuTx: u ∈ Tx.

An exact proof term for the current goal is (andEL (u ∈ Tx) (dense_in u X Tx) Hup).

We prove the intermediate claim Hclu: dense_in u X Tx.

An exact proof term for the current goal is (andER (u ∈ Tx) (dense_in u X Tx) Hup).

We prove the intermediate claim HTsub: Tx ⊆ 𝒫 X.

An exact proof term for the current goal is (topology_subset_axiom X Tx HTx).

We prove the intermediate claim HuPow: u ∈ 𝒫 X.

An exact proof term for the current goal is (HTsub u HuTx).

We prove the intermediate claim HusubX: u ⊆ X.

An exact proof term for the current goal is (PowerE X u HuPow).

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

Apply andI to the current goal.

An exact proof term for the current goal is (closed_of_open_complement X Tx u HTx HuTx).

We prove the intermediate claim Hdual: interior_of X Tx (X ∖ u) = X ∖ closure_of X Tx (X ∖ (X ∖ u)).

An exact proof term for the current goal is (interior_closure_complement_duality X Tx (X ∖ u) HTx (setminus_Subq X u)).

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

rewrite the current goal using (setminus_setminus_eq X u HusubX) (from left to right).

We prove the intermediate claim HcluEq: closure_of X Tx u = X.

An exact proof term for the current goal is Hclu.

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

We prove the intermediate claim Hxx: X ∖ X = Empty.

Apply Empty_Subq_eq to the current goal.

Let z be given.

Assume Hz: z ∈ X ∖ X.

We will prove z ∈ Empty.

We prove the intermediate claim HzX: z ∈ X.

An exact proof term for the current goal is (setminusE1 X X z Hz).

We prove the intermediate claim HznotX: z ∉ X.

An exact proof term for the current goal is (setminusE2 X X z Hz).

Apply FalseE to the current goal.

An exact proof term for the current goal is (HznotX HzX).

An exact proof term for the current goal is Hxx.

We prove the intermediate claim HintUnion: interior_of X Tx (⋃ Fam) = Empty.

An exact proof term for the current goal is ((andER (topology_on X Tx) (∀Fam0 : set, countable_set Fam0 → (∀A : set, A ∈ Fam0 → closed_in X Tx A ∧ interior_of X Tx A = Empty) → interior_of X Tx (⋃ Fam0) = Empty) HBc) Fam HFamcount HFamprop).

We prove the intermediate claim HsubU: ∀u : set, u ∈ U → u ⊆ X.

Let u be given.

Assume Hu: u ∈ U.

We prove the intermediate claim HuTx: u ∈ Tx.

An exact proof term for the current goal is (HUsub u Hu).

An exact proof term for the current goal is (topology_elem_subset X Tx u HTx HuTx).

We prove the intermediate claim HUnionEq: ⋃ Fam = X ∖ (intersection_over_family X U).

An exact proof term for the current goal is (union_of_complements_eq_complement_of_intersection_over_family X U HsubU).

We prove the intermediate claim HintUnion2: interior_of X Tx (X ∖ (intersection_over_family X U)) = Empty.

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

An exact proof term for the current goal is HintUnion.

We prove the intermediate claim Hdual: interior_of X Tx (X ∖ (intersection_over_family X U)) = X ∖ closure_of X Tx (X ∖ (X ∖ (intersection_over_family X U))).

An exact proof term for the current goal is (interior_closure_complement_duality X Tx (X ∖ (intersection_over_family X U)) HTx (setminus_Subq X (intersection_over_family X U))).

We prove the intermediate claim HintUnion3: X ∖ closure_of X Tx (intersection_over_family X U) = Empty.

We prove the intermediate claim HintSub: intersection_over_family X U ⊆ X.

Let z be given.

Assume Hz: z ∈ intersection_over_family X U.

An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ ∀u0 : set, u0 ∈ U → z0 ∈ u0) z Hz).

rewrite the current goal using (setminus_setminus_eq X (intersection_over_family X U) HintSub) (from right to left).

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

An exact proof term for the current goal is HintUnion2.

Apply (set_ext (closure_of X Tx (intersection_over_family X U)) X) to the current goal.

An exact proof term for the current goal is (closure_in_space X Tx (intersection_over_family X U) HTx).

Let x be given.

Assume HxX: x ∈ X.

We will prove x ∈ closure_of X Tx (intersection_over_family X U).

Apply (xm (x ∈ closure_of X Tx (intersection_over_family X U))) to the current goal.

Assume H.

An exact proof term for the current goal is H.

Assume Hnot: x ∉ closure_of X Tx (intersection_over_family X U).

Apply FalseE to the current goal.

We prove the intermediate claim Hxminus: x ∈ X ∖ closure_of X Tx (intersection_over_family X U).

Apply setminusI to the current goal.

An exact proof term for the current goal is HxX.

An exact proof term for the current goal is Hnot.

We prove the intermediate claim HxE: x ∈ Empty.

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

An exact proof term for the current goal is Hxminus.

An exact proof term for the current goal is (EmptyE x HxE).