Let y be given.

Assume Hy: y ∈ closure_of Y (subspace_topology X Tx Y) A.

We will prove y ∈ (closure_of X Tx A) ∩ Y.

We prove the intermediate claim HyY: y ∈ Y.

An exact proof term for the current goal is (SepE1 Y (λy0 ⇒ ∀U : set, U ∈ subspace_topology X Tx Y → y0 ∈ U → U ∩ A ≠ Empty) y Hy).

We prove the intermediate claim HysubCond: ∀U : set, U ∈ subspace_topology X Tx Y → y ∈ U → U ∩ A ≠ Empty.

An exact proof term for the current goal is (SepE2 Y (λy0 ⇒ ∀U : set, U ∈ subspace_topology X Tx Y → y0 ∈ U → U ∩ A ≠ Empty) y Hy).

Apply binintersectI to the current goal.

We will prove y ∈ closure_of X Tx A.

We prove the intermediate claim HyX: y ∈ X.

An exact proof term for the current goal is (HY y HyY).

We prove the intermediate claim HyCond: ∀V : set, V ∈ Tx → y ∈ V → V ∩ A ≠ Empty.

Let V be given.

Assume HV: V ∈ Tx.

Assume HyV: y ∈ V.

We will prove V ∩ A ≠ Empty.

Set U to be the term V ∩ Y.

We prove the intermediate claim HU: U ∈ subspace_topology X Tx Y.

We prove the intermediate claim HUinPower: U ∈ 𝒫 Y.

Apply PowerI to the current goal.

An exact proof term for the current goal is (binintersect_Subq_2 V Y).

We prove the intermediate claim HPred: ∃W ∈ Tx, U = W ∩ Y.

We use V to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HV.

Use reflexivity.

An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 ⇒ ∃W ∈ Tx, U0 = W ∩ Y) U HUinPower HPred).

We prove the intermediate claim HyU: y ∈ U.

Apply binintersectI to the current goal.

An exact proof term for the current goal is HyV.

An exact proof term for the current goal is HyY.

We prove the intermediate claim HUA_ne: U ∩ A ≠ Empty.

An exact proof term for the current goal is (HysubCond U HU HyU).

We will prove V ∩ A ≠ Empty.

Assume HVA_empty: V ∩ A = Empty.

We prove the intermediate claim HUA_sub_VA: U ∩ A ⊆ V ∩ A.

Let z be given.

Assume Hz: z ∈ U ∩ A.

We prove the intermediate claim HzU: z ∈ U.

An exact proof term for the current goal is (binintersectE1 U A z Hz).

We prove the intermediate claim HzV: z ∈ V.

An exact proof term for the current goal is (binintersectE1 V Y z HzU).

We prove the intermediate claim HzA: z ∈ A.

An exact proof term for the current goal is (binintersectE2 U A z Hz).

An exact proof term for the current goal is (binintersectI V A z HzV HzA).

We prove the intermediate claim HUA_sub_Empty: U ∩ A ⊆ Empty.

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

An exact proof term for the current goal is HUA_sub_VA.

We prove the intermediate claim HUA_empty: U ∩ A = Empty.

An exact proof term for the current goal is (Empty_Subq_eq (U ∩ A) HUA_sub_Empty).

An exact proof term for the current goal is (HUA_ne HUA_empty).

An exact proof term for the current goal is (SepI X (λy0 ⇒ ∀V : set, V ∈ Tx → y0 ∈ V → V ∩ A ≠ Empty) y HyX HyCond).

An exact proof term for the current goal is HyY.

Let y be given.

Assume Hy: y ∈ (closure_of X Tx A) ∩ Y.

We will prove y ∈ closure_of Y (subspace_topology X Tx Y) A.

We prove the intermediate claim HyClX: y ∈ closure_of X Tx A.

An exact proof term for the current goal is (binintersectE1 (closure_of X Tx A) Y y Hy).

We prove the intermediate claim HyY: y ∈ Y.

An exact proof term for the current goal is (binintersectE2 (closure_of X Tx A) Y y Hy).

We prove the intermediate claim HyXCond: ∀V : set, V ∈ Tx → y ∈ V → V ∩ A ≠ Empty.

An exact proof term for the current goal is (SepE2 X (λy0 ⇒ ∀V : set, V ∈ Tx → y0 ∈ V → V ∩ A ≠ Empty) y HyClX).

We prove the intermediate claim HySubCond: ∀U : set, U ∈ subspace_topology X Tx Y → y ∈ U → U ∩ A ≠ Empty.

Let U be given.

Assume HU: U ∈ subspace_topology X Tx Y.

Assume HyU: y ∈ U.

We will prove U ∩ A ≠ Empty.

We prove the intermediate claim HUex: ∃V ∈ Tx, U = V ∩ Y.

An exact proof term for the current goal is (subspace_topologyE X Tx Y U HU).

Apply HUex to the current goal.

Let V be given.

Assume HVandEq.

Apply HVandEq to the current goal.

Assume HV: V ∈ Tx.

Assume HUeq: U = V ∩ Y.

We prove the intermediate claim HyV: y ∈ V.

We prove the intermediate claim HyVY: y ∈ V ∩ Y.

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

An exact proof term for the current goal is HyU.

An exact proof term for the current goal is (binintersectE1 V Y y HyVY).

We prove the intermediate claim HVA_ne: V ∩ A ≠ Empty.

An exact proof term for the current goal is (HyXCond V HV HyV).

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

We will prove (V ∩ Y) ∩ A ≠ Empty.

Assume HVYAempty: (V ∩ Y) ∩ A = Empty.

We prove the intermediate claim HVA_sub_VYA: V ∩ (Y ∩ A) ⊆ V ∩ A.

Let z be given.

Assume Hz: z ∈ V ∩ (Y ∩ A).

We prove the intermediate claim HzV: z ∈ V.

An exact proof term for the current goal is (binintersectE1 V (Y ∩ A) z Hz).

We prove the intermediate claim HzYA: z ∈ Y ∩ A.

An exact proof term for the current goal is (binintersectE2 V (Y ∩ A) z Hz).

We prove the intermediate claim HzA: z ∈ A.

An exact proof term for the current goal is (binintersectE2 Y A z HzYA).

An exact proof term for the current goal is (binintersectI V A z HzV HzA).

We prove the intermediate claim HVYAeq: V ∩ (Y ∩ A) = (V ∩ Y) ∩ A.

Apply set_ext to the current goal.

Let z be given.

Assume Hz: z ∈ V ∩ (Y ∩ A).

We prove the intermediate claim HzV: z ∈ V.

An exact proof term for the current goal is (binintersectE1 V (Y ∩ A) z Hz).

We prove the intermediate claim HzYA: z ∈ Y ∩ A.

An exact proof term for the current goal is (binintersectE2 V (Y ∩ A) z Hz).

We prove the intermediate claim HzY: z ∈ Y.

An exact proof term for the current goal is (binintersectE1 Y A z HzYA).

We prove the intermediate claim HzA: z ∈ A.

An exact proof term for the current goal is (binintersectE2 Y A z HzYA).

We prove the intermediate claim HzVY: z ∈ V ∩ Y.

An exact proof term for the current goal is (binintersectI V Y z HzV HzY).

An exact proof term for the current goal is (binintersectI (V ∩ Y) A z HzVY HzA).

Let z be given.

Assume Hz: z ∈ (V ∩ Y) ∩ A.

We prove the intermediate claim HzVY: z ∈ V ∩ Y.

An exact proof term for the current goal is (binintersectE1 (V ∩ Y) A z Hz).

We prove the intermediate claim HzV: z ∈ V.

An exact proof term for the current goal is (binintersectE1 V Y z HzVY).

We prove the intermediate claim HzY: z ∈ Y.

An exact proof term for the current goal is (binintersectE2 V Y z HzVY).

We prove the intermediate claim HzA: z ∈ A.

An exact proof term for the current goal is (binintersectE2 (V ∩ Y) A z Hz).

We prove the intermediate claim HzYA: z ∈ Y ∩ A.

An exact proof term for the current goal is (binintersectI Y A z HzY HzA).

An exact proof term for the current goal is (binintersectI V (Y ∩ A) z HzV HzYA).

We prove the intermediate claim HVYAempty2: V ∩ (Y ∩ A) = Empty.

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

An exact proof term for the current goal is HVYAempty.

We prove the intermediate claim Hex_w: ∃w : set, w ∈ V ∩ A.

Apply (dneg (∃w : set, w ∈ V ∩ A)) to the current goal.

Assume Hnot: ¬ (∃w : set, w ∈ V ∩ A).

We prove the intermediate claim HVAempty: V ∩ A = Empty.

Apply Empty_Subq_eq to the current goal.

Let w be given.

Assume Hw: w ∈ V ∩ A.

Apply FalseE to the current goal.

Apply Hnot to the current goal.

We use w to witness the existential quantifier.

An exact proof term for the current goal is Hw.

An exact proof term for the current goal is (HVA_ne HVAempty).

Apply Hex_w to the current goal.

Let w be given.

Assume Hw: w ∈ V ∩ A.

We prove the intermediate claim HwV: w ∈ V.

An exact proof term for the current goal is (binintersectE1 V A w Hw).

We prove the intermediate claim HwA: w ∈ A.

An exact proof term for the current goal is (binintersectE2 V A w Hw).

We prove the intermediate claim HwY: w ∈ Y.

An exact proof term for the current goal is (HA w HwA).

We prove the intermediate claim HwYA: w ∈ Y ∩ A.

An exact proof term for the current goal is (binintersectI Y A w HwY HwA).

We prove the intermediate claim HwVYA: w ∈ V ∩ (Y ∩ A).

An exact proof term for the current goal is (binintersectI V (Y ∩ A) w HwV HwYA).

We prove the intermediate claim HVYAnonempty: V ∩ (Y ∩ A) ≠ Empty.

Assume HVYAempty_contra: V ∩ (Y ∩ A) = Empty.

We prove the intermediate claim Hwempty: w ∈ Empty.

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

An exact proof term for the current goal is HwVYA.

An exact proof term for the current goal is (EmptyE w Hwempty False).

An exact proof term for the current goal is (HVYAnonempty HVYAempty2).

An exact proof term for the current goal is (SepI Y (λy0 ⇒ ∀U : set, U ∈ subspace_topology X Tx Y → y0 ∈ U → U ∩ A ≠ Empty) y HyY HySubCond).